The Definition of Depth

In this section, we give the definition of depth of a module over a local ring. We also extablished some basic facts about it using the Rees theorem proven above. In this section, we set R be a noetherian commutative ring, all modules refer to R-module.

Main definition and results

• moduleDepth : The depth between two R-modules defined as the minimal nontrivial Ext between them, equal to ⊤ : ℕ∞ if no such index.

• Ideal.depth : The depth of a R-module M with respect to an ideal I, defined as moduleDepth (R⧸ I, M).

• IsLocalRing.depth : For a local ring R, the depth of a R-module with respect to the maximal ideal.

• moduleDepth_eq_depth_of_supp_eq : For I : Ideal R, if support of a finitely generated module N is equal to PrimeSpectrum.zeroLocus I, then for any finitely generated nontrivial module M with IM < M, moduleDepth N M = I.depth M

• moduleDepth_eq_sSup_length_regular : For I : Ideal R, nontrivial finitely generated module M and N, if support of Nis equal toPrimeSpectrum.zeroLocus IandIM < M, moduleDepth N Mis equal to the supremum of length ofM-regular sequence in I`

• IsLocalRing.depth_quotSMulTop_succ_eq_moduleDepth : For R local, a R-module M and a M-regular element x in maximalIdeal R, IsLocalRing.depth (QuotSMulTop x M) + 1 = IsLocalRing.depth M

• moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth : For R local, a R-module M and a M-regular sequence rs in maximalIdeal R, moduleDepth N (M ⧸ (Ideal.ofList rs) • (⊤ : Submodule R M)) + rs.length = moduleDepth N M

noncomputable def moduleDepth {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) : ℕ∞

The depth between two R-modules defined as the minimal nontrivial Ext between them.

Equations

• moduleDepth N M = sSup {n : ℕ∞ | ∀ (i : ℕ), ↑i < n → Subsingleton (CategoryTheory.Abelian.Ext N M i)}

noncomputable def Ideal.depth {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) (M : ModuleCat R) : ℕ∞

The depth of a R-module M with respect to an ideal I, defined as moduleDepth (R⧸ I, M).

Equations

• I.depth M = moduleDepth (ModuleCat.of R (Shrink.{?u.7, ?u.6} (R ⧸ I))) M

noncomputable def IsLocalRing.depth {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : ModuleCat R) : ℕ∞

For a local ring R, the depth of a R-module with respect to the maximal ideal.

Equations

• IsLocalRing.depth M = (IsLocalRing.maximalIdeal R).depth M

theorem moduleDepth_eq_find {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) (h : ∃ (n : ℕ), Nontrivial (CategoryTheory.Abelian.Ext N M n)) : moduleDepth N M = ↑(Nat.find h)

theorem moduleDepth_eq_top_iff {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) : moduleDepth N M = ⊤ ↔ ∀ (i : ℕ), Subsingleton (CategoryTheory.Abelian.Ext N M i)

theorem Ideal.depth_eq_top_of_subsingleton {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) (M : ModuleCat R) (sub : Subsingleton ↑M) : I.depth M = ⊤

theorem IsLocalRing.depth_eq_top_of_subsingleton {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : ModuleCat R) (sub : Subsingleton ↑M) : depth M = ⊤

theorem moduleDepth_lt_top_iff {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) : moduleDepth N M < ⊤ ↔ ∃ (n : ℕ), Nontrivial (CategoryTheory.Abelian.Ext N M n)

theorem moduleDepth_eq_iff {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) (n : ℕ) : moduleDepth N M = ↑n ↔ Nontrivial (CategoryTheory.Abelian.Ext N M n) ∧ ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i)

theorem ext_subsingleton_of_lt_moduleDepth {R : Type u} [CommRing R] [Small.{v, u} R] {N M : ModuleCat R} {i : ℕ} (lt : ↑i < moduleDepth N M) : Subsingleton (CategoryTheory.Abelian.Ext N M i)

theorem moduleDepth_eq_sup_nat {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) : moduleDepth N M = sSup {n : ℕ∞ | n < ⊤ ∧ ∀ (i : ℕ), ↑i < n → Subsingleton (CategoryTheory.Abelian.Ext N M i)}

theorem moduleDepth_eq_depth_of_supp_eq {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (N M : ModuleCat R) [Module.Finite R ↑M] [Nfin : Module.Finite R ↑N] [Nntr : Nontrivial ↑N] (smul_lt : I • ⊤ < ⊤) (hsupp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I) : moduleDepth N M = I.depth M

theorem moduleDepth_eq_of_iso_fst {R : Type u} [CommRing R] [Small.{v, u} R] (M : ModuleCat R) {N N' : ModuleCat R} (e : N ≅ N') : moduleDepth N M = moduleDepth N' M

theorem moduleDepth_eq_of_iso_snd {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) {M M' : ModuleCat R} (e : M ≅ M') : moduleDepth N M = moduleDepth N M'

theorem Ideal.depth_eq_of_iso {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) {M M' : ModuleCat R} (e : M ≅ M') : I.depth M = I.depth M'

theorem IsLocalRing.depth_eq_of_iso {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] {M M' : ModuleCat R} (e : M ≅ M') : depth M = depth M'

theorem moduleDepth_eq_zero_of_hom_nontrivial {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) : moduleDepth N M = 0 ↔ Nontrivial (↑N →ₗ[R] ↑M)

theorem moduleDepth_ge_min_of_shortExact_snd_fst {R : Type u} [CommRing R] [Small.{v, u} R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (N : ModuleCat R) : moduleDepth S.X₂ N ≥ min (moduleDepth S.X₁ N) (moduleDepth S.X₃ N)

theorem moduleDepth_ge_min_of_shortExact_fst_fst {R : Type u} [CommRing R] [Small.{v, u} R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (N : ModuleCat R) : moduleDepth S.X₁ N ≥ min (moduleDepth S.X₂ N) (moduleDepth S.X₃ N - 1)

theorem moduleDepth_ge_min_of_shortExact_trd_fst {R : Type u} [CommRing R] [Small.{v, u} R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (N : ModuleCat R) : moduleDepth S.X₃ N ≥ min (moduleDepth S.X₂ N) (moduleDepth S.X₁ N + 1)

theorem moduleDepth_ge_min_of_shortExact_snd_snd {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) : moduleDepth N S.X₂ ≥ min (moduleDepth N S.X₁) (moduleDepth N S.X₃)

theorem moduleDepth_ge_min_of_shortExact_fst_snd {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) : moduleDepth N S.X₁ ≥ min (moduleDepth N S.X₂) (moduleDepth N S.X₃ + 1)

theorem moduleDepth_ge_min_of_shortExact_trd_snd {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) : moduleDepth N S.X₃ ≥ min (moduleDepth N S.X₂) (moduleDepth N S.X₁ - 1)

theorem moduleDepth_eq_sSup_length_regular {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (N M : ModuleCat R) [Module.Finite R ↑M] [Nfin : Module.Finite R ↑N] [Nntr : Nontrivial ↑N] (smul_lt : I • ⊤ < ⊤) (hsupp : Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I) : moduleDepth N M = sSup {x : ℕ∞ | ∃ (rs : List R) (_ : RingTheory.Sequence.IsRegular (↑M) rs) (_ : ∀ r ∈ rs, r ∈ I), ↑rs.length = x}

theorem IsLocalRing.ideal_depth_eq_sSup_length_regular {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (I : Ideal R) (netop : I ≠ ⊤) (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] : I.depth M = sSup {x : ℕ∞ | ∃ (rs : List R) (_ : RingTheory.Sequence.IsRegular (↑M) rs) (_ : ∀ r ∈ rs, r ∈ I), ↑rs.length = x}

theorem IsLocalRing.depth_eq_sSup_length_regular {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] [Nontrivial ↑M] : depth M = sSup {x : ℕ∞ | ∃ (rs : List R) (_ : RingTheory.Sequence.IsRegular (↑M) rs) (_ : ∀ r ∈ rs, r ∈ maximalIdeal R), ↑rs.length = x}

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

theorem Submodule.comap_lt_top_of_lt_range {R : Type u} [CommRing R] {M : Type u_1} {N : Type u_2} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (f : M →ₗ[R] N) (p : Submodule R N) (lt : p < f.range) : comap f p < ⊤

theorem moduleDepth_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] [Small.{w, u} R] {N M : Type v} {N' M' : Type w} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup N] [Module R N] [Module.Finite R N] [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [AddCommGroup N'] [Module R N'] [Module.Finite R N'] [Nontrivial N] (eM : M ≃ₗ[R] M') (eN : N ≃ₗ[R] N') (I : Ideal R) (smul_lt : I • ⊤ < ⊤) (hsupp : Module.support R N = PrimeSpectrum.zeroLocus ↑I) : moduleDepth (ModuleCat.of R N) (ModuleCat.of R M) = moduleDepth (ModuleCat.of R N') (ModuleCat.of R M')

theorem Ideal.depth_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] [Small.{w, u} R] {M : Type v} {M' : Type w} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup M'] [Module R M'] [Module.Finite R M'] (eM : M ≃ₗ[R] M') (I : Ideal R) (smul_lt : I • ⊤ < ⊤) : I.depth (ModuleCat.of R M) = I.depth (ModuleCat.of R M')

theorem IsLocalRing.depth_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] [Small.{w, u} R] {M : Type v} {M' : Type w} [AddCommGroup M] [Module R M] [Module.Finite R M] [AddCommGroup M'] [Module R M'] [Module.Finite R M'] [IsLocalRing R] [Nontrivial M] (eM : M ≃ₗ[R] M') : depth (ModuleCat.of R M) = depth (ModuleCat.of R M')

theorem ring_depth_shrink_eq {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (lt_top : I < ⊤) : I.depth (ModuleCat.of R (Shrink.{v, u} R)) = I.depth (ModuleCat.of R R)

theorem moduleDepth_quotSMulTop_succ_eq_moduleDepth {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) (x : R) (reg : IsSMulRegular (↑M) x) (mem : x ∈ Module.annihilator R ↑N) : moduleDepth N (ModuleCat.of R (QuotSMulTop x ↑M)) + 1 = moduleDepth N M

theorem Ideal.depth_quotSMulTop_succ_eq_moduleDepth {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) (M : ModuleCat R) (x : R) (reg : IsSMulRegular (↑M) x) (mem : x ∈ I) : I.depth (ModuleCat.of R (QuotSMulTop x ↑M)) + 1 = I.depth M

theorem IsLocalRing.depth_quotSMulTop_succ_eq_moduleDepth {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : ModuleCat R) (x : R) (reg : IsSMulRegular (↑M) x) (mem : x ∈ maximalIdeal R) : depth (ModuleCat.of R (QuotSMulTop x ↑M)) + 1 = depth M

theorem moduleDepth_quotient_regular_sequence_add_length_eq_moduleDepth {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) (rs : List R) (reg : RingTheory.Sequence.IsWeaklyRegular (↑M) rs) (h : ∀ r ∈ rs, r ∈ Module.annihilator R ↑N) : moduleDepth N (ModuleCat.of R (↑M ⧸ Ideal.ofList rs • ⊤)) + ↑rs.length = moduleDepth N M

theorem ideal_depth_quotient_regular_sequence_add_length_eq_ideal_depth {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) (M : ModuleCat R) (rs : List R) (reg : RingTheory.Sequence.IsWeaklyRegular (↑M) rs) (h : ∀ r ∈ rs, r ∈ I) : I.depth (ModuleCat.of R (↑M ⧸ Ideal.ofList rs • ⊤)) + ↑rs.length = I.depth M

theorem depth_quotient_regular_sequence_add_length_eq_depth {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] (M : ModuleCat R) (rs : List R) (reg : RingTheory.Sequence.IsRegular (↑M) rs) : IsLocalRing.depth (ModuleCat.of R (↑M ⧸ Ideal.ofList rs • ⊤)) + ↑rs.length = IsLocalRing.depth M

theorem IsLocalRing.depth_eq_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsLocalRing R] [IsNoetherianRing R] [IsLocalRing R'] [IsNoetherianRing R'] (e : R ≃+* R') : depth (ModuleCat.of R R) = depth (ModuleCat.of R' R')

theorem IsLocalRing.depth_eq_of_algebraMap_surjective {R : Type u} [CommRing R] [Small.{v, u} R] [IsLocalRing R] [IsNoetherianRing R] {S : Type u} [CommRing S] [IsLocalRing S] [Algebra R S] [Small.{v, u} S] [IsNoetherianRing S] (M : Type v) [AddCommGroup M] [Module R M] [Module.Finite R M] [Module S M] [IsScalarTower R S M] [Nontrivial M] (surj : Function.Surjective ⇑(algebraMap R S)) : depth (ModuleCat.of R M) = depth (ModuleCat.of S M)

theorem IsLocalRing.depth_quotient_regular_succ_eq_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (x : R) (reg : IsSMulRegular R x) (mem : x ∈ maximalIdeal R) : depth (ModuleCat.of (R ⧸ x • ⊤) (R ⧸ x • ⊤)) + 1 = depth (ModuleCat.of R R)

theorem IsLocalRing.depth_quotient_span_regular_succ_eq_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (x : R) (reg : IsSMulRegular R x) (mem : x ∈ maximalIdeal R) : depth (ModuleCat.of (R ⧸ Ideal.span {x}) (R ⧸ Ideal.span {x})) + 1 = depth (ModuleCat.of R R)

theorem IsLocalRing.depth_quotient_regular_sequence_add_length_eq_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (rs : List R) (reg : RingTheory.Sequence.IsWeaklyRegular R rs) (mem : ∀ r ∈ rs, r ∈ maximalIdeal R) : depth (ModuleCat.of (R ⧸ Ideal.ofList rs) (R ⧸ Ideal.ofList rs)) + ↑rs.length = depth (ModuleCat.of R R)