Depth as the supremum of lengths of weakly regular sequences

Mathlib defines the depth I.depth M of a module M with respect to an ideal I through the vanishing of Ext (R ⧸ I) M, and identifies it, for a finite module over a Noetherian ring with I M ≠ M, with the supremum of the lengths of M-regular sequences in I. Stacks defines the I-depth of a module through regular sequences, and the convenient form with no hypothesis on I M uses weakly regular sequences, which do not ask that M ⧸ (f₁, …, fᵣ) M be nonzero.

This file proves that, for every finite module M over a Noetherian ring and every ideal I, I.depth M is the supremum in ℕ∞ of the lengths of weakly M-regular sequences in I, and that the depth is infinite exactly when I M = M. Over a Noetherian local ring this says that IsLocalRing.depth M is the supremum of the lengths of weakly M-regular sequences in the maximal ideal, and that it is infinite exactly when M = 0.

Main results

• Ideal.depth_le_height: I.depth M is at most the height of every prime of the support of M containing I.
• Ideal.depth_lt_top: if I M ≠ M then I.depth M is finite.
• Ideal.depth_eq_top_iff: I.depth M = ⊤ if and only if I M = M.
• Ideal.depth_eq_sSup_length_isWeaklyRegular: I.depth M is the supremum of the lengths of weakly M-regular sequences in I.
• Ideal.exists_isWeaklyRegular_of_le_depth: a module of depth at least n with respect to I has a weakly regular sequence of length n in I.
• IsLocalRing.depth_eq_top_iff: over a Noetherian local ring, depth M = ⊤ if and only if M = 0.
• IsLocalRing.depth_eq_sSup_length_isWeaklyRegular: over a Noetherian local ring, depth M is the supremum of the lengths of weakly M-regular sequences in the maximal ideal.
• IsLocalRing.exists_isWeaklyRegular_of_le_depth: over a Noetherian local ring, a module of depth at least n has a weakly regular sequence of length n in the maximal ideal.

References

• Stacks Project, Definition 10.72.1

theorem Ideal.depth_eq_top_of_smul_top_eq_top {R : Type u} [CommRing R] [Small.{v, u} R] (I : Ideal R) (M : ModuleCat R) [Module.Finite R ↑M] (hI : I • ⊤ = ⊤) : I.depth M = ⊤

If I M = M for a finite module M, then Ext (R ⧸ I) M vanishes in every degree, so the depth of M with respect to I is infinite.

theorem Ideal.depth_le_height {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (M : ModuleCat R) [Module.Finite R ↑M] (p : Ideal R) [p.IsPrime] (hIp : I ≤ p) (hMp : Module.annihilator R ↑M ≤ p) : I.depth M ≤ p.height

Let M be a finite module over a Noetherian ring and p a prime ideal in the support of M containing I. Then the depth of M with respect to I is at most the height of p.

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

Let M be a finite module over a Noetherian ring and I an ideal with I M ≠ M. Then the depth of M with respect to I is finite.

theorem Ideal.depth_eq_top_iff {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (M : ModuleCat R) [Module.Finite R ↑M] : I.depth M = ⊤ ↔ I • ⊤ = ⊤

For a finite module M over a Noetherian ring, the depth of M with respect to I is infinite exactly when I M = M.

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

For a finite module M over a Noetherian ring and an ideal I, the depth of M with respect to I is the supremum of the lengths of weakly M-regular sequences in I. Unlike Ideal.depth_eq_sSup_length_isRegular, this needs no hypothesis I M ≠ M: when I M = M both sides are ⊤.

theorem Ideal.exists_isWeaklyRegular_of_le_depth {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (M : ModuleCat R) [Module.Finite R ↑M] {n : ℕ} (h : ↑n ≤ I.depth M) : ∃ (rs : List R), rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsWeaklyRegular (↑M) rs

Let M be a finite module over a Noetherian ring and I an ideal. If the depth of M with respect to I is at least n, then M has a weakly regular sequence of length n in I.

theorem IsLocalRing.depth_eq_top_iff {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] : depth M = ⊤ ↔ Subsingleton ↑M

A finite module over a Noetherian local ring has infinite depth exactly when it is zero.

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

The depth of a finite module over a Noetherian local ring is the supremum of the lengths of weakly M-regular sequences in the maximal ideal.

theorem IsLocalRing.exists_isWeaklyRegular_of_le_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] {n : ℕ} (h : ↑n ≤ depth M) : ∃ (rs : List R), rs.length = n ∧ (∀ r ∈ rs, r ∈ maximalIdeal R) ∧ RingTheory.Sequence.IsWeaklyRegular (↑M) rs

A finite module of depth at least n over a Noetherian local ring has a weakly regular sequence of length n in the maximal ideal.