Definition of Cohen-Macaulay Ring

In this file, we define a R-module M is Cohen Macaulay module if it is zero or Module.supportDim R M = IsLocalRing.depth M. We also define a local ring R IsCohenMacaulayLocalRing if ringKrullDim R = IsLocalRing.depth (ModuleCat.of R R), a commutative ring is Cohen Macaulay if its localization at every prime IsCohenMacaulayLocalRing.

Main definition and results

• ModuleCat.IsCohenMacaulay : A R-module M is Cohen Macaulay if it is zero or Module.supportDim R M = IsLocalRing.depth M.

• isLocalize_at_prime_dim_eq_prime_depth_of_isCohenMacaulay : For any prime ideal p and finitely generated R-module M, Module.supportDim Rₚ Mₚ = p.depth M

• isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay : For any prime ideal p and finitely generated R-module M, Mₚ is Cohen Macaulay as Rₚ module.

• IsCohenMacaulayLocalRing : A local ring is Cohen Macaulay if ringKrullDim R = IsLocalRing.depth (ModuleCat.of R R).

• IsCohenMacaulayRing : A commutative ring is Cohen Macaulay if its localization at every prime IsCohenMacaulayLocalRing

• isCohenMacaulayRing_iff : A commutative ring is Cohen Macaulay iff its localization at every maximal ideal IsCohenMacaulayLocalRing

class ModuleCat.IsCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) : Prop

A R-module M is Cohen Macaulay if it is zero or Module.supportDim R M = IsLocalRing.depth M.

• depth_eq_dim : Subsingleton ↑M ∨ Module.supportDim R ↑M = ↑(IsLocalRing.depth M)

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

theorem ModuleCat.depth_eq_supportDim_of_cohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [cm : M.IsCohenMacaulay] [ntr : Nontrivial ↑M] : Module.supportDim R ↑M = ↑(IsLocalRing.depth M)

theorem ModuleCat.depth_eq_supportDim_unbot_of_cohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [cm : M.IsCohenMacaulay] [ntr : Nontrivial ↑M] : (Module.supportDim R ↑M).unbot ⋯ = IsLocalRing.depth M

theorem ModuleCat.IsCohenMacaulay_of_iso {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] {M M' : ModuleCat R} (e : M ≅ M') [M.IsCohenMacaulay] : M'.IsCohenMacaulay

theorem depth_eq_dim_quotient_associated_prime_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [Small.{v, u} R] (M : ModuleCat R) [M.IsCohenMacaulay] [Module.Finite R ↑M] [Nontrivial ↑M] (mem : p ∈ associatedPrimes R ↑M) : IsLocalRing.depth M = (ringKrullDim (R ⧸ p)).unbot ⋯

theorem associated_prime_minimal_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [Small.{v, u} R] (M : ModuleCat R) [M.IsCohenMacaulay] [Module.Finite R ↑M] [Nontrivial ↑M] (mem : p ∈ associatedPrimes R ↑M) : p ∈ (Module.annihilator R ↑M).minimalPrimes

theorem associated_prime_eq_minimalPrimes_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [M.IsCohenMacaulay] [Module.Finite R ↑M] [Nontrivial ↑M] : associatedPrimes R ↑M = (Module.annihilator R ↑M).minimalPrimes

theorem quotSMulTop_isCohenMacaulay_iff_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] (r : R) (reg : IsSMulRegular (↑M) r) (mem : r ∈ IsLocalRing.maximalIdeal R) : M.IsCohenMacaulay ↔ (ModuleCat.of R (QuotSMulTop r ↑M)).IsCohenMacaulay

theorem quotient_regular_isCohenMacaulay_iff_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] (rs : List R) (reg : RingTheory.Sequence.IsRegular (↑M) rs) : M.IsCohenMacaulay ↔ (ModuleCat.of R (↑M ⧸ Ideal.ofList rs • ⊤)).IsCohenMacaulay

@[reducible, inline]

abbrev SemiLinearMapAlgebraMapOfLinearMap {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₗ[R] N) : M →ₛₗ[algebraMap R A] N

Turn a R-linear map into algebraMap R A-semilinear map if its target is an A-module.

Equations

• SemiLinearMapAlgebraMapOfLinearMap f = { toAddHom := f.toAddHom, map_smul' := ⋯ }

@[reducible, inline]

abbrev LinearMapOfSemiLinearMapAlgebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] [Module A N] [IsScalarTower R A N] (f : M →ₛₗ[algebraMap R A] N) : M →ₗ[R] N

Turn a algebraMap R A-semilinear map into a R-linear map.

Equations

• LinearMapOfSemiLinearMapAlgebraMap f = { toAddHom := f.toAddHom, map_smul' := ⋯ }

@[reducible, inline]

abbrev quotSMulTop_isLocalizedModule_map {R : Type u} [CommRing R] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] (x : R) (M : Type u_1) [AddCommGroup M] [Module R M] (Mₚ : Type u_2) [AddCommGroup Mₚ] [Module R Mₚ] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] (f : M →ₗ[R] Mₚ) : QuotSMulTop x M →ₗ[R] QuotSMulTop ((algebraMap R Rₚ) x) Mₚ

Given R-algebra Rₚ, R-module M and Rₚ-module Mₚ and f : M →ₗ[R] Mₚ, The linear map QuotSMulTop x M →ₗ[R] QuotSMulTop ((algebraMap R Rₚ) x) Mₚ lifted from f.

Equations

• quotSMulTop_isLocalizedModule_map Rₚ x M Mₚ f = LinearMapOfSemiLinearMapAlgebraMap ((x • ⊤).mapQ ((algebraMap R Rₚ) x • ⊤) (SemiLinearMapAlgebraMapOfLinearMap f) ⋯)

theorem isLocalizedModule_quotSMulTop_isLocalizedModule_map {R : Type u} [CommRing R] (p : Ideal R) [p.IsPrime] (Rₚ : Type u') [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] (x : R) (M : Type u_1) [AddCommGroup M] [Module R M] (Mₚ : Type u_2) [AddCommGroup Mₚ] [Module R Mₚ] [Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ] (f : M →ₗ[R] Mₚ) [IsLocalizedModule.AtPrime p f] : IsLocalizedModule.AtPrime p (quotSMulTop_isLocalizedModule_map Rₚ x M Mₚ f)

theorem isLocalization_at_prime_prime_depth_le_depth {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [Small.{v, u} R] [p.IsPrime] {Rₚ : Type u'} [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [Small.{v', u'} Rₚ] [IsNoetherianRing Rₚ] (M : ModuleCat R) (Mₚ : ModuleCat Rₚ) [Module R ↑Mₚ] [IsScalarTower R Rₚ ↑Mₚ] (f : ↑M →ₗ[R] ↑Mₚ) [IsLocalizedModule.AtPrime p f] [IsLocalRing Rₚ] [Module.Finite R ↑M] [ntr : Nontrivial ↑Mₚ] : p.depth M ≤ IsLocalRing.depth Mₚ

theorem isLocalize_at_prime_dim_eq_prime_depth_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [Small.{v, u} R] [p.IsPrime] {Rₚ : Type u'} [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [IsNoetherianRing Rₚ] (M : ModuleCat R) (Mₚ : ModuleCat Rₚ) [Module R ↑Mₚ] [IsScalarTower R Rₚ ↑Mₚ] (f : ↑M →ₗ[R] ↑Mₚ) [IsLocalizedModule.AtPrime p f] [Module.Finite R ↑M] [M.IsCohenMacaulay] [ntr : Nontrivial ↑Mₚ] : Module.supportDim Rₚ ↑Mₚ = ↑(p.depth M)

theorem isLocalize_at_prime_isCohenMacaulay_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [Small.{v, u} R] [p.IsPrime] {Rₚ : Type u'} [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [Small.{v', u'} Rₚ] [IsNoetherianRing Rₚ] (M : ModuleCat R) (Mₚ : ModuleCat Rₚ) [Module R ↑Mₚ] [IsScalarTower R Rₚ ↑Mₚ] (f : ↑M →ₗ[R] ↑Mₚ) [IsLocalizedModule.AtPrime p f] [IsLocalRing Rₚ] [Module.Finite R ↑M] [M.IsCohenMacaulay] : Mₚ.IsCohenMacaulay

theorem isLocalize_at_prime_depth_eq_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [Small.{v, u} R] [p.IsPrime] {Rₚ : Type u'} [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [Small.{v', u'} Rₚ] [IsNoetherianRing Rₚ] (M : ModuleCat R) (Mₚ : ModuleCat Rₚ) [Module R ↑Mₚ] [IsScalarTower R Rₚ ↑Mₚ] (f : ↑M →ₗ[R] ↑Mₚ) [IsLocalizedModule.AtPrime p f] [IsLocalRing Rₚ] [Module.Finite R ↑M] [Nontrivial ↑Mₚ] [M.IsCohenMacaulay] : p.depth M = IsLocalRing.depth Mₚ

theorem localize_at_prime_isCohenMacaulay_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [M.IsCohenMacaulay] : (ModuleCat.of (Localization.AtPrime p) (LocalizedModule.AtPrime p ↑M)).IsCohenMacaulay

theorem localize_at_prime_depth_eq_of_isCohenMacaulay {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [M.IsCohenMacaulay] [Nontrivial (LocalizedModule.AtPrime p ↑M)] : p.depth M = IsLocalRing.depth (ModuleCat.of (Localization.AtPrime p) (LocalizedModule.AtPrime p ↑M))

class IsCohenMacaulayLocalRing (R : Type u) [CommRing R] extends IsLocalRing R : Prop

A local ring is Cohen Macaulay if ringKrullDim R = IsLocalRing.depth (ModuleCat.of R R).

• exists_pair_ne : ∃ (x : R) (y : R), x ≠ y
• isUnit_or_isUnit_of_add_one {a b : R} (h : a + b = 1) : IsUnit a ∨ IsUnit b
• depth_eq_dim : ringKrullDim R = ↑(IsLocalRing.depth (ModuleCat.of R R))

theorem isCohenMacaulayLocalRing_def (R : Type u) [CommRing R] [IsLocalRing R] : IsCohenMacaulayLocalRing R ↔ ringKrullDim R = ↑(IsLocalRing.depth (ModuleCat.of R R))

theorem isCohenMacaulayLocalRing_of_ringKrullDim_le_depth (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (le : ringKrullDim R ≤ ↑(IsLocalRing.depth (ModuleCat.of R R))) : IsCohenMacaulayLocalRing R

theorem isCohenMacaulayLocalRing_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsNoetherianRing R] (e : R ≃+* R') [CM : IsCohenMacaulayLocalRing R] : IsCohenMacaulayLocalRing R'

theorem isCohenMacaulayLocalRing_iff (R : Type u) [CommRing R] [IsLocalRing R] : IsCohenMacaulayLocalRing R ↔ (ModuleCat.of R R).IsCohenMacaulay

instance instIsCohenMacaulayOf (R : Type u) [CommRing R] [IsCohenMacaulayLocalRing R] : (ModuleCat.of R R).IsCohenMacaulay

theorem isCohenMacaulayLocalRing_localization_atPrime (R : Type u) [CommRing R] [IsCohenMacaulayLocalRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime] (Rₚ : Type u_1) [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] : IsCohenMacaulayLocalRing Rₚ

theorem associatedPrimes_self_eq_minimalPrimes (R : Type u) [CommRing R] [IsCohenMacaulayLocalRing R] [IsNoetherianRing R] : associatedPrimes R R = minimalPrimes R

class IsCohenMacaulayRing (R : Type u) [CommRing R] : Prop

A commutative ring is Cohen Macaulay if its localization at every prime IsCohenMacaulayLocalRing.

• CM_localize (p : Ideal R) (x✝ : p.IsPrime) : IsCohenMacaulayLocalRing (Localization.AtPrime p)

theorem isCohenMacaulayRing_def (R : Type u) [CommRing R] : IsCohenMacaulayRing R ↔ ∀ (p : Ideal R) (x : p.IsPrime), IsCohenMacaulayLocalRing (Localization.AtPrime p)

theorem isCohenMacaulayRing_def' (R : Type u) [CommRing R] : IsCohenMacaulayRing R ↔ ∀ (p : PrimeSpectrum R), IsCohenMacaulayLocalRing (Localization.AtPrime p.asIdeal)

theorem isCohenMacaulayRing_iff (R : Type u) [CommRing R] [IsNoetherianRing R] : IsCohenMacaulayRing R ↔ ∀ (m : Ideal R) (x : m.IsMaximal), IsCohenMacaulayLocalRing (Localization.AtPrime m)

theorem isCohenMacaulayRing_of_ringEquiv {R : Type u_1} {R' : Type u_2} [CommRing R] [CommRing R'] [IsNoetherianRing R] (e : R ≃+* R') [CM : IsCohenMacaulayRing R] : IsCohenMacaulayRing R'

theorem IsCohenMacaulayRing.of_isCohenMacaulayLocalRing (R : Type u) [CommRing R] [IsCohenMacaulayLocalRing R] [IsNoetherianRing R] : IsCohenMacaulayRing R

theorem IsCohenMacaulayLocalRing.of_isLocalRing_of_isCohenMacaulayRing (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] [IsCohenMacaulayRing R] : IsCohenMacaulayLocalRing R

theorem quotient_regular_smul_top_isCohenMacaulay_iff_isCohenMacaulay (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (x : R) (reg : IsSMulRegular R x) (mem : x ∈ IsLocalRing.maximalIdeal R) : IsCohenMacaulayLocalRing R ↔ IsCohenMacaulayLocalRing (R ⧸ x • ⊤)

theorem quotient_span_regular_isCohenMacaulay_iff_isCohenMacaulay (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (x : R) (reg : IsSMulRegular R x) (mem : x ∈ IsLocalRing.maximalIdeal R) : IsCohenMacaulayLocalRing R ↔ IsCohenMacaulayLocalRing (R ⧸ Ideal.span {x})

theorem quotient_regular_sequence_isCohenMacaulay_iff_isCohenMacaulay (R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (rs : List R) (reg : RingTheory.Sequence.IsWeaklyRegular R rs) (mem : ∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) : IsCohenMacaulayLocalRing R ↔ IsCohenMacaulayLocalRing (R ⧸ Ideal.ofList rs)