The Ischebeck theorem and its corollary

theorem moduleDepth_ge_depth_sub_dim {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (M N : ModuleCat R) [Module.Finite R ↑M] [Nfin : Module.Finite R ↑N] [Nontrivial ↑M] [Nntr : Nontrivial ↑N] [Small.{v, u} R] : moduleDepth N M ≥ IsLocalRing.depth M - (Module.supportDim R ↑N).unbot ⋯

theorem quotient_prime_ringKrullDim_ne_bot {R : Type u} [CommRing R] {P : Ideal R} (prime : P.IsPrime) : ringKrullDim (R ⧸ P) ≠ ⊥

theorem depth_le_ringKrullDim_associatedPrime {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] (P : Ideal R) (ass : P ∈ associatedPrimes R ↑M) : IsLocalRing.depth M ≤ (ringKrullDim (R ⧸ P)).unbot ⋯

theorem depth_le_supportDim {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] : ↑(IsLocalRing.depth M) ≤ Module.supportDim R ↑M

theorem depth_le_ringKrullDim {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] : ↑(IsLocalRing.depth M) ≤ ringKrullDim R

theorem depth_ne_top {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] : IsLocalRing.depth M ≠ ⊤