Krull Dimension of quotient regular sequence

Main results

• Module.supportDim_add_length_eq_supportDim_of_isRegular: If M is a finite module over a Noetherian local ring R, r₁, …, rₙ is an M-sequence, then dim M/(r₁, …, rₙ)M + n = dim M.

theorem Module.exists_ltSeries_support_isMaximal_last_of_ltSeries_support {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] (q : LTSeries ↑(support R M)) : ∃ (p : LTSeries ↑(support R M)), q.length ≤ p.length ∧ (↑(RelSeries.last p)).asIdeal.IsMaximal

theorem Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (h : x ∈ (annihilator R M).jacobson) : supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1

theorem Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p) : supportDim R (QuotSMulTop x M) + 1 ≤ supportDim R M

If M is a finite module over a commutative ring R, x ∈ M is not in any minimal prime of M, then dim M/xM + 1 ≤ dim M.

theorem Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p) (hx : x ∈ (annihilator R M).jacobson) : supportDim R (QuotSMulTop x M) + 1 = supportDim R M

theorem Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (reg : IsSMulRegular M x) (hx : x ∈ (annihilator R M).jacobson) : supportDim R (QuotSMulTop x M) + 1 = supportDim R M

theorem ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson {R : Type u_1} [CommRing R] [IsNoetherianRing R] {x : R} (reg : IsSMulRegular R x) (hx : x ∈ Ring.jacobson R) : ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R

theorem ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_jacobson {R : Type u_1} [CommRing R] [IsNoetherianRing R] {x : R} (reg : IsSMulRegular R x) (hx : x ∈ Ring.jacobson R) : ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] [IsNoetherianRing R] {r : R} (hr : r ∈ nonZeroDivisors R) {p : Ideal R} [p.IsPrime] (h : ↑p.height = ringKrullDim R) (hp : r ∈ p) : ringKrullDim (R ⧸ Ideal.span {r}) + 1 = ringKrullDim R

If r is a nonzerodivisor contained in an ideal of maximal height, dim (R / (r)) + 1 = dim R.

theorem Module.supportDim_le_supportDim_quotSMulTop_succ {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] [IsLocalRing R] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) : supportDim R M ≤ supportDim R (QuotSMulTop x M) + 1

If M is a finite module over a Noetherian local ring R, then dim M ≤ dim M/xM + 1 for every x in the maximal ideal of the local ring R.

theorem ringKrullDim_le_ringKrullDim_quotSMulTop_succ {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) : ringKrullDim R ≤ ringKrullDim (R ⧸ x • ⊤) + 1

@[deprecated ringKrullDim_le_ringKrullDim_quotient_add_card (since := "2026-01-12")]

theorem ringKrullDim_le_ringKrullDim_add_card {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {S : Finset R} (hS : ↑S ⊆ ↑(IsLocalRing.maximalIdeal R)) : ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span ↑S) + ↑S.card

@[deprecated ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (since := "2026-01-12")]

theorem ringKrullDim_le_ringKrullDim_add_spanFinrank {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {I : Ideal R} (h : I ≠ ⊤) : ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

theorem Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] [IsLocalRing R] {x : R} (hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p) (hx : x ∈ IsLocalRing.maximalIdeal R) : supportDim R (QuotSMulTop x M) + 1 = supportDim R M

Stacks Tag 0B52 (the equality case)

theorem Module.supportDim_quotSMulTop_succ_eq_supportDim {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] [IsLocalRing R] {x : R} (reg : IsSMulRegular M x) (hx : x ∈ IsLocalRing.maximalIdeal R) : supportDim R (QuotSMulTop x M) + 1 = supportDim R M

theorem ringKrullDim_quotSMulTop_succ_eq_ringKrullDim {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {x : R} (reg : IsSMulRegular R x) (hx : x ∈ IsLocalRing.maximalIdeal R) : ringKrullDim (QuotSMulTop x R) + 1 = ringKrullDim R

theorem ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {x : R} (reg : IsSMulRegular R x) (hx : x ∈ IsLocalRing.maximalIdeal R) : ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

theorem ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim_of_mem_nonZeroDivisors {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] {x : R} (reg : x ∈ nonZeroDivisors R) (hx : x ∈ IsLocalRing.maximalIdeal R) : ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R

Stacks Tag 00KW

theorem Module.supportDim_add_length_eq_supportDim_of_isRegular {R : Type u_1} [CommRing R] [IsNoetherianRing R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] [IsLocalRing R] (rs : List R) (reg : RingTheory.Sequence.IsRegular M rs) : supportDim R (M ⧸ Ideal.ofList rs • ⊤) + ↑rs.length = supportDim R M

If M is a finite module over a Noetherian local ring R, r₁, …, rₙ is an M-sequence, then dim M/(r₁, …, rₙ)M + n = dim M.

theorem ringKrullDim_add_length_eq_ringKrullDim_of_isRegular {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] (rs : List R) (reg : RingTheory.Sequence.IsRegular R rs) : ringKrullDim (R ⧸ Ideal.ofList rs) + ↑rs.length = ringKrullDim R