Cohen–Macaulay modules over a local ring

A finite module M over a Noetherian local ring R is Cohen–Macaulay if M = 0 or its depth equals the dimension of its support (Stacks, Definition 10.103.1 (00N3)). Depth is Mathlib's IsLocalRing.depth, defined through the vanishing of Ext (R ⧸ 𝔪) M, and the dimension of the support is Mathlib's Module.supportDim. Since the depth of a finite nonzero module never exceeds the dimension of its support (IsLocalRing.depth_le_supportDim), being Cohen–Macaulay is the reverse inequality.

The zero module is Cohen–Macaulay by convention: its depth is ⊤ while its support dimension is ⊥, so the depth equation alone would exclude it.

Main definitions and results

• Module.IsCohenMacaulay R M: the R-module M is Cohen–Macaulay.
• Module.isCohenMacaulay_iff_supportDim_le_depth: a finite nonzero module over a Noetherian local ring is Cohen–Macaulay if and only if the dimension of its support is at most its depth.
• RingEquiv.isCohenMacaulay_self_iff: being Cohen–Macaulay over itself is invariant under isomorphisms of Noetherian local rings.
• Module.isCohenMacaulay_iff_isCohenMacaulay_of_surjective: along a surjective homomorphism of local rings R → T, a finite T-module is Cohen–Macaulay over R exactly when it is over T. For instance, a quotient R ⧸ I that is Cohen–Macaulay as an R-module is a Cohen–Macaulay ring.
• IsLocalization.AtPrime.isCohenMacaulay_self_iff: a localization of a Noetherian ring at a prime is Cohen–Macaulay over itself exactly when Localization.AtPrime p is.
• Module.isCohenMacaulay_quotSMulTop_iff: for an M-regular element x of the maximal ideal, M ⧸ x M is Cohen–Macaulay if and only if M is (Stacks, Lemma 10.103.5 (0C6G)), and Module.isCohenMacaulay_quotient_ofList_smul_iff is the same for an M-regular sequence.
• Module.isCohenMacaulay_of_krullDimLE_zero: every module over a Noetherian local ring of dimension zero, such as a field, is Cohen–Macaulay.
• Module.isCohenMacaulay_self_of_isDomain_of_krullDimLE_one: a Noetherian local domain of dimension at most one, such as a discrete valuation ring, is Cohen–Macaulay over itself.
• Module.IsCohenMacaulay.ringKrullDim_quotient_eq_supportDim and Module.IsCohenMacaulay.associatedPrimes_eq_minimalPrimes: a Cohen–Macaulay module is unmixed. For every associated prime p, the dimension of R ⧸ p is the dimension of the support, and the associated primes are exactly the minimal primes of the support, so there are no embedded primes (Stacks, Lemma 10.103.7 (0BUS)).

def Module.IsCohenMacaulay (R : Type u) [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : Type v) [AddCommGroup M] [Module R M] : Prop

An R-module M over a local ring R is Cohen–Macaulay if it is zero or its depth equals the dimension of its support. This is meant for finite modules over a Noetherian local ring, where the depth never exceeds the dimension of the support. Stacks, Definition 10.103.1 (00N3).

theorem Module.isCohenMacaulay_iff (R : Type u) [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : Type v) [AddCommGroup M] [Module R M] : IsCohenMacaulay R M ↔ Subsingleton M ∨ ↑(IsLocalRing.depth ↧M) = supportDim R M

Unfolds Module.IsCohenMacaulay.

theorem Module.isCohenMacaulay_of_subsingleton {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Subsingleton M] : IsCohenMacaulay R M

The zero module is Cohen–Macaulay.

theorem Module.isCohenMacaulay_iff_depth_eq {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial M] : IsCohenMacaulay R M ↔ ↑(IsLocalRing.depth ↧M) = supportDim R M

A nonzero module is Cohen–Macaulay if and only if its depth equals the dimension of its support.

theorem Module.IsCohenMacaulay.depth_eq {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Nontrivial M] (h : IsCohenMacaulay R M) : ↑(IsLocalRing.depth ↧M) = supportDim R M

The depth of a nonzero Cohen–Macaulay module equals the dimension of its support.

theorem Module.isCohenMacaulay_iff_supportDim_le_depth {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] [Nontrivial M] : IsCohenMacaulay R M ↔ supportDim R M ≤ ↑(IsLocalRing.depth ↧M)

A finite nonzero module over a Noetherian local ring is Cohen–Macaulay if and only if the dimension of its support is at most its depth, the reverse inequality being IsLocalRing.depth_le_supportDim.

theorem LinearEquiv.isCohenMacaulay_iff {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] [Small.{w, u} R] {M : Type v} [AddCommGroup M] [Module R M] {N : Type w} [AddCommGroup N] [Module R N] (e : M ≃ₗ[R] N) : Module.IsCohenMacaulay R M ↔ Module.IsCohenMacaulay R N

Being Cohen–Macaulay is invariant under linear equivalence.

theorem RingEquiv.isCohenMacaulay_self_iff {R : Type u} {S : Type v} [CommRing R] [CommRing S] [IsLocalRing R] [IsLocalRing S] [IsNoetherianRing R] (e : R ≃+* S) : Module.IsCohenMacaulay R R ↔ Module.IsCohenMacaulay S S

A Noetherian local ring is Cohen–Macaulay over itself exactly when an isomorphic ring is.

theorem Module.isCohenMacaulay_iff_isCohenMacaulay_of_surjective {R : Type u} {T : Type v} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [CommRing T] [IsLocalRing T] [Algebra R T] {M : Type w} [AddCommGroup M] [Module R M] [Module T M] [IsScalarTower R T M] [Module.Finite T M] [Small.{w, u} R] [Small.{w, v} T] (hsurj : Function.Surjective ⇑(algebraMap R T)) : IsCohenMacaulay R M ↔ IsCohenMacaulay T M

Along a surjective homomorphism of local rings R → T with R Noetherian, a finite T-module is Cohen–Macaulay over R exactly when it is Cohen–Macaulay over T: both the depth and the dimension of the support are unchanged by restriction of scalars.

theorem IsLocalization.AtPrime.isCohenMacaulay_self_iff {A : Type u} [CommRing A] [IsNoetherianRing A] (p : Ideal A) [p.IsPrime] (B : Type v) [CommRing B] [IsLocalRing B] [Algebra A B] [IsLocalization.AtPrime B p] : Module.IsCohenMacaulay B B ↔ Module.IsCohenMacaulay (Localization.AtPrime p) (Localization.AtPrime p)

A localization B of a Noetherian ring A at a prime p is Cohen–Macaulay over itself exactly when Localization.AtPrime p is. The local-ring instance on B is taken as an argument so that it can be the one already present, as on the stalks of a scheme; it always holds, by IsLocalization.AtPrime.isLocalRing.

theorem Module.isCohenMacaulay_quotSMulTop_iff {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] {x : R} (reg : IsSMulRegular M x) (hx : x ∈ IsLocalRing.maximalIdeal R) : IsCohenMacaulay R (QuotSMulTop x M) ↔ IsCohenMacaulay R M

For an M-regular element x of the maximal ideal, M ⧸ x M is Cohen–Macaulay if and only if M is. Stacks, Lemma 10.103.5 (0C6G).

theorem Module.isCohenMacaulay_quotient_ofList_smul_iff {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] (rs : List R) (reg : RingTheory.Sequence.IsRegular M rs) : IsCohenMacaulay R (M ⧸ Ideal.ofList rs • ⊤) ↔ IsCohenMacaulay R M

For an M-regular sequence r₁, …, rₙ, M ⧸ (r₁, …, rₙ) M is Cohen–Macaulay if and only if M is. Stacks, Lemma 10.103.5 (0C6G), applied n times.

theorem Module.isCohenMacaulay_of_krullDimLE_zero {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] {M : Type v} [AddCommGroup M] [Module R M] [Ring.KrullDimLE 0 R] : IsCohenMacaulay R M

Every module over a Noetherian local ring of dimension zero is Cohen–Macaulay.

theorem Module.IsCohenMacaulay.ringKrullDim_quotient_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] (h : IsCohenMacaulay R M) {p : Ideal R} (hp : IsAssociatedPrime p M) : ringKrullDim (R ⧸ p) = supportDim R M

Over a Noetherian local ring, the quotient by an associated prime of a Cohen–Macaulay module has the dimension of the support of the module. Stacks, Lemma 10.103.7 (0BUS); H. Matsumura, Commutative Ring Theory, Theorem 17.3 (i).

theorem Module.IsCohenMacaulay.associatedPrimes_eq_minimalPrimes {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) : associatedPrimes R M = (annihilator R M).minimalPrimes

The associated primes of a Cohen–Macaulay module over a Noetherian local ring are the minimal primes of its support: a Cohen–Macaulay module has no embedded primes. Stacks, Lemma 10.103.7 (0BUS).

theorem Module.isCohenMacaulay_self_of_isDomain_of_krullDimLE_one {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsDomain R] [Ring.KrullDimLE 1 R] : IsCohenMacaulay R R

A Noetherian local domain of dimension at most one is Cohen–Macaulay over itself.