CohenMacaulayModule.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 0 contain sorry, 0 declared as axioms

Small and big Cohen-Macaulay modules

Let R be a local ring. A small Cohen-Macaulay module, also called a maximal Cohen-Macaulay module, is a finitely generated nonzero R-module M such that some system of parameters of R is a regular sequence on M. A balanced big Cohen-Macaulay module is an R-module W, not necessarily finitely generated, with m • W ≠ W and such that every system of parameters of R is a regular sequence on W. Over a Noetherian local ring the two notions agree for finitely generated modules.

Both definitions are only intended for Noetherian local rings, where systems of parameters exist.

Main declarations

Module.IsSmallCohenMacaulay R M: M is a small Cohen-Macaulay R-module.
Module.IsBalancedBigCohenMacaulay R W: W is a balanced big Cohen-Macaulay R-module.

Imports (1)

FormalConjecturesForMathlib.RingTheory.SystemOfParameters

Imported by 1 file

FormalConjecturesForMathlib.lean

structure Module.IsSmallCohenMacaulay Documented declaration: IsSmallCohenMacaulay line 53 source
Source documentation
A small Cohen-Macaulay module over a local ring R is a finitely generated R-module M, necessarily nonzero, such that some system of parameters of R is a regular sequence on M. Such a module is also called a maximal Cohen-Macaulay module. Nonzeroness is automatic, see Module.IsSmallCohenMacaulay.nontrivial.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module
3 instances, coercions and auxiliary constants left out.
```
structure IsSmallCohenMacaulay : Prop where
…
```
structure Module.IsBalancedBigCohenMacaulay Documented declaration: IsBalancedBigCohenMacaulay line 69 source
Source documentation
A balanced big Cohen-Macaulay module over a local ring R is an R-module M, not necessarily finitely generated, with m • M ≠ M and such that every system of parameters of R is a regular sequence on M.
Part of the literature calls this simply a big Cohen-Macaulay module, and reserves the weaker condition that some system of parameters is a regular sequence for that name. Over a Noetherian local ring the field smul_top_ne_top follows from isRegular, see Module.smul_top_ne_top_of_isRegular.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module
3 instances, coercions and auxiliary constants left out.
```
structure IsBalancedBigCohenMacaulay : Prop where
…
```
theorem Module.IsSmallCohenMacaulay.nontrivial A small Cohen-Macaulay module is nonzero: a regular sequence on M is one for which M is not killed by the ideal it generates line 81 source
Source documentation
A small Cohen-Macaulay module is nonzero: a regular sequence on M is one for which M is not killed by the ideal it generates.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Module.IsSmallCohenMacaulay, Nontrivial
Proof uses: List, And, IsLocalRing.IsSystemOfParameters, RingTheory.Sequence.IsRegular, Exists, Module.IsSmallCohenMacaulay.exists_isRegular, Classical.byContradiction, Not, RingTheory.Sequence.IsRegular.top_ne_smul, Subsingleton.elim, Submodule, Iff.mpr, Subsingleton, Submodule.subsingleton_iff, Eq.mp, congrArg, propext, not_nontrivial_iff_subsingleton, Top.top, HSMul.hSMul and 2 more
17 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem IsSmallCohenMacaulay.nontrivial (h : IsSmallCohenMacaulay R M) : Nontrivial M := by
…
```
Mentions: Module.IsSmallCohenMacaulay
theorem Module.IsBalancedBigCohenMacaulay.nontrivial A balanced big Cohen-Macaulay module is nonzero: on the zero module the maximal ideal acts by the identity line 91 source
Source documentation
A balanced big Cohen-Macaulay module is nonzero: on the zero module the maximal ideal acts by the identity.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, Module.IsBalancedBigCohenMacaulay, Nontrivial
Proof uses: Classical.byContradiction, Not, Module.IsBalancedBigCohenMacaulay.smul_top_ne_top, Subsingleton.elim, Submodule, Iff.mpr, Subsingleton, Submodule.subsingleton_iff, Eq.mp, congrArg, propext, not_nontrivial_iff_subsingleton, HSMul.hSMul, Ideal, IsLocalRing.maximalIdeal, Top.top
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem IsBalancedBigCohenMacaulay.nontrivial (h : IsBalancedBigCohenMacaulay R M) :
    Nontrivial M := by
…
```
Mentions: Module.IsBalancedBigCohenMacaulay
theorem Module.smul_top_ne_top_of_isRegular Documented declaration: smul_top_ne_top_of_isRegular line 102 source
Source documentation
Over a Noetherian local ring, m • M ≠ M follows from the regularity of a single system of parameters, because the ideal that a system of parameters generates contains a power of the maximal ideal.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: CommRing, IsLocalRing, AddCommGroup, Module, IsNoetherianRing, List, IsLocalRing.IsSystemOfParameters, RingTheory.Sequence.IsRegular, Ne, Submodule, HSMul.hSMul, Ideal, IsLocalRing.maximalIdeal, Top.top
Proof uses: Eq, Nat, LE.le, HPow.hPow, Ideal.ofList, Exists, False, Ideal.exists_pow_le_of_le_radical_of_fg, Eq.ge, Ideal.radical, IsLocalRing.IsSystemOfParameters.radical_eq, IsNoetherian.noetherian, Nat.recAux, of_eq_true, OfNat.ofNat, Eq.trans, True, congrFun', congrArg, pow_zero and 16 more
58 instances, coercions and auxiliary constants left out.

Tactic trace: 8 steps
Open to load the checked before-and-after goal states.
```
theorem smul_top_ne_top_of_isRegular [IsNoetherianRing R] {rs : List R}
    (hrs : IsSystemOfParameters R rs) (h : RingTheory.Sequence.IsRegular M rs) :
    maximalIdeal R • (⊤ : Submodule R M) ≠ ⊤ := by
…
```
theorem Module.isSmallCohenMacaulay_self Over a field K, the module K is a small Cohen-Macaulay module line 116 source
Source documentation
Over a field K, the module K is a small Cohen-Macaulay module.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Field, Module.IsSmallCohenMacaulay
Proof uses: Module.IsSmallCohenMacaulay.mk, inferInstance, Module.Finite, Exists.intro, List, And, IsLocalRing.IsSystemOfParameters, RingTheory.Sequence.IsRegular, List.nil, And.intro, IsLocalRing.isSystemOfParameters_nil, PrimeSpectrum, RingTheory.Sequence.IsRegular.nil
25 instances, coercions and auxiliary constants left out.
```
theorem isSmallCohenMacaulay_self (K : Type*) [Field K] : IsSmallCohenMacaulay K K where
…
```
Mentions: Module.IsSmallCohenMacaulay