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.
regular local rings are domains and cohen macaulay
Statement
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 .
Facts & Assumptions
Given: The objects and hypotheses in the statement. We work with the Axiom of Choice; cited dependent-choice and resolution-existence hypotheses are retained.
regular local domain induction: Every regular local ring is an integral domain.
regular local parameter is nonzerodivisor: In a positive-dimensional regular local ring, every member of a regular system of parameters is a nonzerodivisor.
regular local quotient by parameter is regular: Let be regular local of dimension , and let . Then is regular local, of dimension and embedding dimension .
Cohen--Macaulay local modules and rings: Let be a Noetherian local ring and let be a nonzero finite -module. The module is Cohen--Macaulay when The zero module is excluded from this local definition. The local ring is Cohen--Macaulay when it is Cohen--Macaulay as an -module.
Regular Sequence On A Module: Let be a commutative unital ring, let be an -module, and let be a finite ordered sequence in . The sequence is -regular when and multiplication by is injective on it for every , and .
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.
Depth with respect to an ideal: For a finite module with , is the supremum of the lengths of -regular sequences in ; for a local ring depth means depth with respect to its maximal ideal.
Proof
The ring is a domain. Successively apply the parameter-quotient lemma: after quotients the remaining cotangent classes form a basis, and the quotient is regular of dimension . This starts with and ends with .
At each nonterminal stage the next parameter is a nonzerodivisor. All the quotients are nonzero, so the tuple satisfies the definition of a regular sequence. Its length is , and the depth definition therefore gives ; the support-dimension bound gives . Thus the Cohen–Macaulay definition holds. For , the empty tuple and the field give the same conclusion.
Depends on
Used by
- regular local ring satisfies s two Corollary
- Cohen–Macaulayness over a finite regular local base Example
- finite residue field projective dimension forces depth equals dimension Lemma
- flat local ascent of regularity Lemma
- regular local residue field koszul resolution Lemma
- auslander buchsbaum serre regularity criterion Theorem
Dependency tree · two levels
16 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
- 10.106.2–10.106.3 (standard reference, not scraped)