Regular sequences in Cohen–Macaulay modules

Let M be a nonzero finite Cohen–Macaulay module over a Noetherian local ring (R, 𝔪). A sequence r₁, …, rₙ of elements of 𝔪 is M-regular if and only if it cuts the dimension of the support down by its length, dim M ⧸ (r₁, …, rₙ) M + n = dim M (Stacks, Proposition 10.103.4 (00N6)). One direction holds for every finite module (Module.supportDim_add_length_eq_supportDim_of_isRegular); the content is the converse, for which the Cohen–Macaulay hypothesis is essential.

The single-element case rests on unmixedness: every associated prime p of a Cohen–Macaulay module satisfies dim R ⧸ p = dim M, so if x is a zero divisor on M, it lies in such a p, which then lies in the support of M ⧸ x M, and the dimension does not drop at all.

The main application is to a local homomorphism R → S of local rings with S Noetherian and Cohen–Macaulay. If r₁, …, rₙ generate the maximal ideal of R and dim S = dim S ⧸ 𝔪_R S + n, then the images of the rᵢ form an S-regular sequence. For a regular local ring R and a regular system of parameters, n = dim R and the hypothesis is the dimension formula dim S = dim R + dim S ⧸ 𝔪_R S of miracle flatness (Stacks, Lemma 10.128.1 (00R4)), whose proof starts from exactly this regular sequence.

The same holds one element at a time, which is the form an induction on dim R uses. If dim S = dim R + dim S ⧸ 𝔪_R S and x ∈ R satisfies dim R ⧸ (x) + 1 = dim R, for instance x ∈ 𝔪 ∖ 𝔪² in a regular local ring, then x is S-regular, S ⧸ x S is a Cohen–Macaulay ring, and R ⧸ (x) → S ⧸ x S again satisfies the dimension formula, since its closed fibre is that of R → S. Regularity of x comes from the fibre inequality dim S ⧸ x S ≤ dim R ⧸ (x) + dim S ⧸ 𝔪_R S, which forces the dimension of S to drop.

For a finite torsion-free algebra B over a Noetherian integrally closed local domain A, the localization B_𝔮 at a maximal ideal need not be finite over A, but going down along A → B gives it the dimension of A, and its closed fibre B_𝔮 ⧸ 𝔪_A B_𝔮 is Artinian. So B_𝔮 satisfies the dimension formula of miracle flatness, and a Cohen–Macaulay B_𝔮 receives a regular sequence from a regular system of parameters of A. In dimension two, normality of B_𝔮 already implies that it is Cohen–Macaulay (Stacks, Lemma 10.157.4 (031S)). This is the input to miracle flatness for the localizations of finite normal algebras over a normal local domain of dimension two, such as a regular local ring of dimension two, as in the proof of purity for regular local rings (Stacks, Lemma 58.21.3 (0BMA)).

Main results

• Module.IsCohenMacaulay.isSMulRegular_of_supportDim_quotSMulTop_lt: an element x with dim M ⧸ x M < dim M is M-regular (Stacks, Lemma 10.103.3 (00N5), part (a)).
• Module.IsCohenMacaulay.isSMulRegular_iff_supportDim_quotSMulTop_lt: for M ≠ 0, this is a characterization of M-regular elements.
• Module.IsCohenMacaulay.quotSMulTop: under the same hypothesis M ⧸ x M is again Cohen–Macaulay (Stacks, Lemma 10.103.3 (00N5), part (b)).
• Module.IsCohenMacaulay.isRegular_iff_supportDim_add_length_eq_supportDim: for M ≠ 0, a sequence in 𝔪 is M-regular if and only if it cuts the dimension of the support down by its length (Stacks, Proposition 10.103.4 (00N6)).
• Module.IsCohenMacaulay.isRegular_of_le_radical: a system of parameters, that is dim M elements of 𝔪 cutting M down to a module supported at the closed point, is M-regular.
• Module.IsCohenMacaulay.isRegular_map_algebraMap: generators of the maximal ideal of R whose number is dim S - dim S ⧸ 𝔪_R S map to an S-regular sequence.
• Module.IsCohenMacaulay.isRegular_map_algebraMap_localization: for a finite torsion-free algebra B over a Noetherian integrally closed local domain A and a maximal ideal 𝔮 of B with B_𝔮 Cohen–Macaulay, dim A generators of the maximal ideal of A map to a B_𝔮-regular sequence.
• Module.IsCohenMacaulay.isSMulRegular_algebraMap, Module.IsCohenMacaulay.quotient_map_span_singleton and Module.IsCohenMacaulay.ringKrullDim_quotient_map_span_singleton_eq: if R → S satisfies the dimension formula dim S = dim R + dim S ⧸ 𝔪_R S with S Cohen–Macaulay, and dim R ⧸ (x) + 1 = dim R, then x is S-regular, S ⧸ x S is a Cohen–Macaulay ring, and R ⧸ (x) → S ⧸ x S again satisfies the dimension formula.
• TauCeti.isRegular_pair_localization_of_isIntegrallyClosed: when A has dimension two and B_𝔮 is a normal domain, B_𝔮 is automatically Cohen–Macaulay, so every pair generating the maximal ideal of A maps to a B_𝔮-regular sequence.

References

• Stacks Project, Section 10.103, Lemma 10.103.3 (00N5) and Proposition 10.103.4 (00N6).
• Stacks Project, Lemma 10.128.1, the first step of its proof.
• Stacks Project, Lemma 58.21.3, the dimension-two case of its proof.

theorem Module.IsCohenMacaulay.isSMulRegular_of_supportDim_quotSMulTop_lt {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] (h : IsCohenMacaulay R M) {x : R} (hx : supportDim R (QuotSMulTop x M) < supportDim R M) : IsSMulRegular M x

In a finite Cohen–Macaulay module over a Noetherian local ring, an element x with dim M ⧸ x M < dim M is M-regular. Stacks, Lemma 10.103.3 (00N5), part (a), where the drop is assumed to be exactly one.

theorem Module.IsCohenMacaulay.isSMulRegular_iff_supportDim_quotSMulTop_lt {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] (h : IsCohenMacaulay R M) (x : R) : IsSMulRegular M x ↔ supportDim R (QuotSMulTop x M) < supportDim R M

For a nonzero finite Cohen–Macaulay module M over a Noetherian local ring, x is M-regular if and only if dim M ⧸ x M < dim M; for x in the maximal ideal the drop is then exactly one (Module.supportDim_quotSMulTop_succ_eq_supportDim).

theorem Module.IsCohenMacaulay.quotSMulTop {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] (h : IsCohenMacaulay R M) {x : R} (hdim : supportDim R (QuotSMulTop x M) < supportDim R M) : IsCohenMacaulay R (QuotSMulTop x M)

If x satisfies dim M ⧸ x M < dim M for a finite Cohen–Macaulay module M over a Noetherian local ring, then M ⧸ x M is Cohen–Macaulay. Stacks, Lemma 10.103.3 (00N5), part (b).

theorem Module.IsCohenMacaulay.isRegular_iff_supportDim_add_length_eq_supportDim {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] [Nontrivial M] (h : IsCohenMacaulay R M) (rs : List R) (hrs : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) : RingTheory.Sequence.IsRegular M rs ↔ supportDim R (M ⧸ Ideal.ofList rs • ⊤) + ↑rs.length = supportDim R M

Regular sequences in a Cohen–Macaulay module. For a nonzero finite Cohen–Macaulay module M over a Noetherian local ring, a sequence r₁, …, rₙ of elements of the maximal ideal is M-regular if and only if dim M ⧸ (r₁, …, rₙ) M + n = dim M. Stacks, Proposition 10.103.4 (00N6).

theorem Module.IsCohenMacaulay.isRegular_of_le_radical {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Module.Finite R M] (h : IsCohenMacaulay R M) {rs : List R} (hrs : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) (hrad : IsLocalRing.maximalIdeal R ≤ (Ideal.ofList rs ⊔ annihilator R M).radical) (hlen : ↑rs.length = supportDim R M) : RingTheory.Sequence.IsRegular M rs

Systems of parameters are regular sequences. Let M be a finite Cohen–Macaulay module over a Noetherian local ring (R, 𝔪); it is nonzero since its dimension is a length. A sequence r₁, …, rₙ of dim M elements of 𝔪 such that (r₁, …, rₙ) + Ann M has radical 𝔪 is M-regular. This is the case of isRegular_iff_supportDim_add_length_eq_supportDim (Stacks, Proposition 10.103.4 (00N6)) in which M ⧸ (r₁, …, rₙ) M is supported at the closed point, hence has dimension zero.

theorem Module.IsCohenMacaulay.isRegular_map_algebraMap {R : Type u_1} {S : Type u} [CommRing R] [IsLocalRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] (hS : IsCohenMacaulay S S) {rs : List R} (hrs : Ideal.ofList rs = IsLocalRing.maximalIdeal R) (hdim : ringKrullDim (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)) + ↑rs.length = ringKrullDim S) : RingTheory.Sequence.IsRegular S (List.map (⇑(algebraMap R S)) rs)

Let R → S be a local homomorphism of local rings with S Noetherian and Cohen–Macaulay. If r₁, …, rₙ generate the maximal ideal of R and dim S ⧸ 𝔪_R S + n = dim S, then the images of the rᵢ form an S-regular sequence. For a regular system of parameters of a regular local ring R, this hypothesis is the dimension formula of miracle flatness (Stacks, Lemma 10.128.1 (00R4)).

theorem Module.IsCohenMacaulay.isSMulRegular_algebraMap {R : Type u_1} {S : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] (hS : IsCohenMacaulay S S) (hdim : ringKrullDim S = ringKrullDim R + ringKrullDim (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) {x : R} (hx : ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R) : IsSMulRegular S ((algebraMap R S) x)

Let R → S be a local homomorphism of Noetherian local rings with S Cohen–Macaulay and dim S = dim R + dim S ⧸ 𝔪_R S. If x ∈ R satisfies dim R ⧸ (x) + 1 = dim R, for instance a nonzero element of the maximal ideal of a regular local ring, then its image in S is S-regular.

theorem Module.IsCohenMacaulay.quotient_map_span_singleton {R : Type u_1} {S : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] (hS : IsCohenMacaulay S S) (hdim : ringKrullDim S = ringKrullDim R + ringKrullDim (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) {x : R} (hx : ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R) [IsLocalRing (S ⧸ Ideal.map (algebraMap R S) (Ideal.span {x}))] : IsCohenMacaulay (S ⧸ Ideal.map (algebraMap R S) (Ideal.span {x})) (S ⧸ Ideal.map (algebraMap R S) (Ideal.span {x}))

Under the hypotheses of Module.IsCohenMacaulay.isSMulRegular_algebraMap, the quotient S ⧸ x S is a Cohen–Macaulay ring.

theorem Module.IsCohenMacaulay.ringKrullDim_quotient_map_span_singleton_eq {R : Type u_1} {S : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing S] [IsLocalRing S] [IsNoetherianRing S] [Algebra R S] [IsLocalHom (algebraMap R S)] (hS : IsCohenMacaulay S S) (hdim : ringKrullDim S = ringKrullDim R + ringKrullDim (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) {x : R} (hx : ringKrullDim (R ⧸ Ideal.span {x}) + 1 = ringKrullDim R) [IsLocalRing (R ⧸ Ideal.span {x})] : ringKrullDim (S ⧸ Ideal.map (algebraMap R S) (Ideal.span {x})) = ringKrullDim (R ⧸ Ideal.span {x}) + ringKrullDim ((S ⧸ Ideal.map (algebraMap R S) (Ideal.span {x})) ⧸ Ideal.map (algebraMap (R ⧸ Ideal.span {x}) (S ⧸ Ideal.map (algebraMap R S) (Ideal.span {x}))) (IsLocalRing.maximalIdeal (R ⧸ Ideal.span {x})))

Under the hypotheses of Module.IsCohenMacaulay.isSMulRegular_algebraMap, the dimension formula dim S = dim R + dim S ⧸ 𝔪_R S passes to the local homomorphism R ⧸ (x) → S ⧸ x S. Together with Module.IsCohenMacaulay.quotient_map_span_singleton, this lets an induction on dim R replace R → S by R ⧸ (x) → S ⧸ x S, as in the proof of miracle flatness (Stacks, Lemma 10.128.1 (00R4)).

theorem Module.IsCohenMacaulay.isRegular_map_algebraMap_localization {A : Type u_1} {B : Type u_2} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [Algebra A B] [Module.Finite A B] [IsTorsionFree A B] {𝔮 : Ideal B} [𝔮.IsMaximal] (h : IsCohenMacaulay (Localization.AtPrime 𝔮) (Localization.AtPrime 𝔮)) {rs : List A} (hrs : Ideal.ofList rs = IsLocalRing.maximalIdeal A) (hlen : ↑rs.length = ringKrullDim A) : RingTheory.Sequence.IsRegular (Localization.AtPrime 𝔮) (List.map (⇑(algebraMap A (Localization.AtPrime 𝔮))) rs)

Let A be a Noetherian integrally closed local domain, B a finite torsion-free A-algebra and 𝔮 a maximal ideal of B such that B_𝔮 is Cohen–Macaulay. If r₁, …, r_d generate the maximal ideal of A, where d = dim A, then their images form a B_𝔮-regular sequence.

theorem TauCeti.isRegular_pair_localization_of_isIntegrallyClosed {A : Type u_1} {B : Type u_2} [CommRing A] [IsLocalRing A] [IsNoetherianRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing B] [Algebra A B] [Module.Finite A B] [Module.IsTorsionFree A B] (hdim : ringKrullDim A = 2) (𝔮 : Ideal B) [𝔮.IsMaximal] [IsDomain (Localization.AtPrime 𝔮)] [IsIntegrallyClosed (Localization.AtPrime 𝔮)] {x y : A} (hxy : Ideal.span {x, y} = IsLocalRing.maximalIdeal A) : RingTheory.Sequence.IsRegular (Localization.AtPrime 𝔮) [(algebraMap A (Localization.AtPrime 𝔮)) x, (algebraMap A (Localization.AtPrime 𝔮)) y]

Let A be a two-dimensional Noetherian integrally closed local domain, B a finite torsion-free A-algebra and 𝔮 a maximal ideal of B such that B_𝔮 is a normal domain. Every pair generating the maximal ideal of A maps to a regular sequence on B_𝔮. Here B need not be local, and B_𝔮 need not be finite over A.