Documentation

Mathlib.RingTheory.Depth.Basic

The Definition of Depth #

In this file, we give the definition of depth of a module over a local ring. We also establish some basic facts about it using the Rees theorem proven in file Mathlib.RingTheory.Depth.Rees. In this file, R will usually be a noetherian commutative ring, all modules refer to R-module.

Main definition and results #

ModuleCat.depth : 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 an R-module M with respect to an ideal I, defined as depth (R ⧸ I) M. This is grade(I, M) in Bruns–Herzog, where "depth" is reserved for the local case below.
IsLocalRing.depth : For a local ring R, the depth of an R-module with respect to the maximal ideal.
ModuleCat.depth_eq_depth_of_support_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, depth N M = I.depth M
ModuleCat.depth_eq_sSup_length_isRegular : For I : Ideal R, nontrivial finitely generated module M and N, if support of N is equal to PrimeSpectrum.zeroLocus I and IM < M, depth N M is equal to the supremum of length of M-regular sequence in I
Ideal.depth_eq_sSup_length_isRegular : For finitely generated module M and an ideal I of Noetherian ring R with IM < M, I.depth M equals to maximal length of M-regular sequences contained in I.

References #

noncomputable def ModuleCat.depth {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

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

Instances For

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

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

Equations

I.depth M = (↧(Shrink.{?u.2, ?u.1} (R ⧸ I))).depth M

Instances For

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 an R-module with respect to the maximal ideal.

Equations

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

Instances For

theorem ModuleCat.depth_eq_top_iff {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) :

N.depth M = ⊤ ↔ ∀ (i : ℕ), Subsingleton (CategoryTheory.Abelian.Ext N M i)

theorem ModuleCat.depth_eq_top_of_subsingleton {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) [Subsingleton ↑M] :

N.depth M = ⊤

theorem Ideal.depth_eq_top_of_subsingleton {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) (M : ModuleCat R) [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) [Subsingleton ↑M] :

theorem ModuleCat.depth_lt_top_iff {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) :

N.depth M < ⊤ ↔ ∃ (n : ℕ), Nontrivial (CategoryTheory.Abelian.Ext N M n)

theorem ModuleCat.depth_eq_iff {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) (n : ℕ) :

N.depth M = ↑n ↔ Nontrivial (CategoryTheory.Abelian.Ext N M n) ∧ ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i)

theorem ModuleCat.subsingleton_ext_of_lt_depth {R : Type u} [CommRing R] [Small.{v, u} R] {N M : ModuleCat R} {i : ℕ} (lt : ↑i < N.depth M) :

Subsingleton (CategoryTheory.Abelian.Ext N M i)

theorem ModuleCat.depth_eq_sSup_lt_top {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) :

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

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

N.depth M = I.depth M

This lemma relates the general depth between two modules and the depth of a module with respect to an ideal, which is used more frequently.

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

N.depth M = N'.depth M

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

N.depth M = N.depth 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 ModuleCat.depth_eq_zero_iff_nontrivial_linearMap {R : Type u} [CommRing R] [Small.{v, u} R] (N M : ModuleCat R) :

N.depth M = 0 ↔ Nontrivial (↑N →ₗ[R] ↑M)

theorem ModuleCat.depth_min_fst_trd_le_snd_left {R : Type u} [CommRing R] [Small.{v, u} R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (N : ModuleCat R) :

min (S.X₁.depth N) (S.X₃.depth N) ≤ S.X₂.depth N

theorem ModuleCat.depth_min_snd_trd_sub_one_le_fst_left {R : Type u} [CommRing R] [Small.{v, u} R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (N : ModuleCat R) :

min (S.X₂.depth N) (S.X₃.depth N - 1) ≤ S.X₁.depth N

theorem ModuleCat.depth_min_snd_fst_add_one_le_trd_left {R : Type u} [CommRing R] [Small.{v, u} R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) (N : ModuleCat R) :

min (S.X₂.depth N) (S.X₁.depth N + 1) ≤ S.X₃.depth N

theorem ModuleCat.depth_min_fst_trd_le_snd_right {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) :

min (N.depth S.X₁) (N.depth S.X₃) ≤ N.depth S.X₂

Stacks Tag 00LX ((1))

theorem ModuleCat.depth_min_snd_trd_add_one_le_fst_right {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) :

min (N.depth S.X₂) (N.depth S.X₃ + 1) ≤ N.depth S.X₁

Stacks Tag 00LX ((3))

theorem ModuleCat.depth_min_snd_fst_sub_one_le_trd_right {R : Type u} [CommRing R] [Small.{v, u} R] (N : ModuleCat R) (S : CategoryTheory.ShortComplex (ModuleCat R)) (hS : S.ShortExact) :

min (N.depth S.X₂) (N.depth S.X₁ - 1) ≤ N.depth S.X₃

Stacks Tag 00LX ((2))

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

N.depth M = sSup {x : ℕ∞ | ∃ (rs : List R) (_ : RingTheory.Sequence.IsRegular (↑M) rs) (_ : ∀ r ∈ rs, r ∈ I), ↑rs.length = x}

theorem Ideal.depth_eq_sSup_length_isRegular {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (M : ModuleCat R) [Module.Finite R ↑M] (smul_lt : I • ⊤ < ⊤) :

I.depth 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_isRegular {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}

Stacks Tag 00LW

theorem Ideal.depth_le_depth_of_le {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] {I J : Ideal R} (h : I ≤ J) (M : ModuleCat R) [Module.Finite R ↑M] (smul_lt : J • ⊤ < ⊤) :

I.depth M ≤ J.depth M

theorem IsLocalRing.depth_eq_sSup_length_isRegular {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 ModuleCat.depth_uliftFunctor_obj {R : Type u} [CommRing R] [Small.{v, u} R] [Small.{max v w, u} R] (N M : ModuleCat R) :

((uliftFunctor.{w, v, u} R).obj N).depth ((uliftFunctor.{w, v, u} R).obj M) = N.depth M

theorem ModuleCat.depth_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [Small.{w, u} R] {N M : Type v} {N' M' : Type w} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N'] (eN : N ≃ₗ[R] N') (eM : M ≃ₗ[R] M') :

(↧N).depth ↧M = (↧N').depth ↧M'

theorem Ideal.depth_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [Small.{w, u} R] {M : Type v} {M' : Type w} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (I : Ideal R) (eM : M ≃ₗ[R] M') :

I.depth ↧M = I.depth ↧M'

theorem IsLocalRing.depth_eq_of_linearEquiv {R : Type u} [CommRing R] [Small.{v, u} R] [Small.{w, u} R] {M : Type v} {M' : Type w} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [IsLocalRing R] (eM : M ≃ₗ[R] M') :

depth ↧M = depth ↧M'

theorem Ideal.depth_shrink {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) :

I.depth ↧(Shrink.{v, u} R) = I.depth ↧R