Maximal Cohen Macaulay Module

The definition of maximal Cohen Macaulay module.

Main definition and results

• isCohenMacaulayLocalRing_of_isRegularLocalRing : regular local ring is Cohen Macaulay

• free_of_isMaximalCohenMacaulay_of_isRegularLocalRing : maximal Cohen Macaulay module over regular local ring is free.

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

A R-module is maximal Cohen Macaulay if IsLocalRing.depth M = ringKrullDim R.

• depth_eq_dim : ↑(IsLocalRing.depth M) = ringKrullDim R

theorem isMaximalCohenMacaulay_def {R : Type u} [CommRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) : M.IsMaximalCohenMacaulay ↔ ↑(IsLocalRing.depth M) = ringKrullDim R

@[instance 100]

instance instNontrivialCarrierOfIsNoetherianRingOfIsMaximalCohenMacaulay {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [M.IsMaximalCohenMacaulay] : Nontrivial ↑M

theorem isCohenMacaulay_of_isMaximalCohenMacaulay {R : Type u} [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [M.IsMaximalCohenMacaulay] : M.IsCohenMacaulay

theorem isCohenMacaulayLocalRing_of_isRegularLocalRing {R : Type u} [CommRing R] [IsRegularLocalRing R] : IsCohenMacaulayLocalRing R

theorem isField_of_isRegularLocalRing_of_dimension_zero {R : Type u} [CommRing R] [IsRegularLocalRing R] (h : ringKrullDim R = 0) : IsField R

theorem free_of_isMaximalCohenMacaulay_of_isRegularLocalRing {R : Type u} [CommRing R] [IsRegularLocalRing R] [Small.{v, u} R] (M : ModuleCat R) [Module.Finite R ↑M] [M.IsMaximalCohenMacaulay] : Module.Free R ↑M