Regular local rings are Cohen–Macaulay

Let (R, 𝔪) be a regular local ring of dimension d, so that 𝔪 is generated by d elements. This file proves that any d elements generating 𝔪 form an R-regular sequence, so that the depth of R equals its dimension and R is Cohen–Macaulay over itself. In particular a regular local ring of dimension at least n has depth at least n, the input that lets results stated for local rings of large depth, such as extension of sections across a closed point, apply to regular local rings.

Main results

• TauCeti.IsRegularLocalRing.isRegular_of_ofList_eq_maximalIdeal: a list of at most spanFinrank 𝔪 elements generating 𝔪, that is, a regular system of parameters, is an R-regular sequence.
• TauCeti.IsRegularLocalRing.depth_eq_ringKrullDim: the depth of a regular local ring over itself is its Krull dimension.
• TauCeti.IsRegularLocalRing.isCohenMacaulay: a regular local ring is Cohen–Macaulay over itself.

The proof is induction on the dimension: the first entry x of a regular system of parameters lies outside 𝔪², so it is a nonzero element of the domain R and R ⧸ (x) is a regular local ring of dimension d - 1, whose maximal ideal is generated by the images of the remaining entries.

References

• The Stacks Project, Lemma 10.106.3.

theorem TauCeti.IsRegularLocalRing.isRegular_of_ofList_eq_maximalIdeal {R : Type u} [CommRing R] [IsRegularLocalRing R] {rs : List R} (hspan : Ideal.ofList rs = IsLocalRing.maximalIdeal R) (hlen : rs.length ≤ Submodule.spanFinrank (IsLocalRing.maximalIdeal R)) : RingTheory.Sequence.IsRegular R rs

A regular system of parameters is a regular sequence. In a regular local ring (R, 𝔪), a list of at most spanFinrank 𝔪 = dim R elements generating 𝔪 (necessarily of exactly that length) is an R-regular sequence. Stacks, Lemma 10.106.3 (00NQ).

theorem TauCeti.IsRegularLocalRing.depth_eq_ringKrullDim {R : Type u} [CommRing R] [IsRegularLocalRing R] : ↑(IsLocalRing.depth ↧R) = ringKrullDim R

The depth of a regular local ring over itself equals its Krull dimension.

theorem TauCeti.IsRegularLocalRing.isCohenMacaulay {R : Type u} [CommRing R] [IsRegularLocalRing R] : Module.IsCohenMacaulay R R

A regular local ring is Cohen–Macaulay. Stacks, Lemma 10.106.3 (00NQ).