Theorems · Theorem · commutative algebra

Module.supportDim_add_length_eq_supportDim_of_isRegular

∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {M : Type u_2} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M] [IsLocalRing R] (rs : List R),
  RingTheory.Sequence.IsRegular M rs →
    Module.supportDim R (M ⧸ Ideal.ofList rs • ⊤) + ↑rs.length = Module.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.

Defined in

Mathlib.RingTheory.KrullDimension.Regular

Cited by

1 results in Mathlib

Foundations

Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsNoetherianRingAddCommGroupModuleModule.FiniteIsLocalRing