How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Cohen–Macaulayness over a finite regular local base
Example
Let be an injective finite local map of nonzero Noetherian local rings, with regular. Then is Cohen–Macaulay if and only if it is free as an -module.
Facts & Assumptions
Given: The objects and hypotheses in the example. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.
auslander buchsbaum formula: For a nonzero finite module of finite projective dimension over a nonzero Noetherian local ring , . Consequently such an with is free.
auslander buchsbaum serre regularity criterion: For a nonzero Noetherian local ring the following are equivalent: is regular; ; ; and every finite -module has finite projective dimension. When these hold, . A nonzero finite module over regular local is maximal Cohen–Macaulay (depth ) if and only if it is free.
Injective integral extensions preserve Krull dimension: Assume the Axiom of Choice. Let be an injective integral extension of nonzero commutative rings. Then .
Every system of parameters is regular in a Cohen--Macaulay module: Every system of parameters of a nonzero finite Cohen--Macaulay module over a Noetherian local ring is a regular sequence on that module.
One regular system of parameters implies Cohen--Macaulayness: Let be finite over a Noetherian local ring. If one system of parameters for is -regular, then is Cohen--Macaulay. Here a system of parameters for means a tuple in the maximal ideal, where , such that has finite length.
regular local rings are domains and cohen macaulay: A regular local ring of dimension is a domain and Cohen–Macaulay. For every regular system , the tuple is -regular and is regular local of dimension for all .
Depth is bounded by support dimension: For every nonzero finite module over a Noetherian local ring , The nonzero hypothesis is essential for this formulation: under the adopted convention , whereas the empty support has no nonnegative Krull dimension.
Assuming the Axiom of Choice, Nakayama's lemma: Assume the Axiom of Choice. Let be a commutative ring, let satisfy , and let be a finitely generated left -module. If , then .
Verification
Finite injectivity makes the extension integral and gives . Choose a regular system of . The quotient is a finite-dimensional algebra over and a nonzero local ring. Its descending powers of the maximal ideal stabilize as vector subspaces; at stabilization Nakayama makes that power zero. Thus , and the images of the are parameters of .
If is Cohen–Macaulay, those parameters are -regular. Regarded as an -module, consequently has depth at least . The support-dimension bound gives depth at most (its annihilator is zero by injectivity). Homological regularity makes its projective dimension over finite; Auslander–Buchsbaum gives projective dimension zero and freeness.
Conversely, if is free over , the regular parameter sequence of remains injective successively on the finite direct sums describing and its successive quotients. The terminal quotient is nonzero. Since this is a system of parameters of , the regular-parameter criterion makes Cohen–Macaulay. If , the sequence is empty and is a field; all steps remain valid.
Depends on
- auslander buchsbaum formula
- auslander buchsbaum serre regularity criterion
- Injective integral extensions preserve Krull dimension
- Every system of parameters is regular in a Cohen--Macaulay module
- One regular system of parameters implies Cohen--Macaulayness
- regular local rings are domains and cohen macaulay
- Depth is bounded by support dimension
- Assuming the Axiom of Choice, Nakayama's lemma
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
31 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Exercise 12.41, p.125 (standard reference, not scraped)
- Corollary 1.63, p.27 (standard reference, not scraped)