Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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 R of dimension d is a domain and Cohen–Macaulay. For every regular system (x1,,xd), the tuple is R-regular and R/(x1,,xc) is regular local of dimension dc for all 0cd.

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.

[F1]

regular local domain induction: Every regular local ring is an integral domain.

[F2]

regular local parameter is nonzerodivisor: In a positive-dimensional regular local ring, every member of a regular system of parameters is a nonzerodivisor.

[F3]

regular local quotient by parameter is regular: Let (R,m,k) be regular local of dimension d, and let xmm2. Then R/(x) is regular local, of dimension and embedding dimension d1.

[F4]

Cohen--Macaulay local modules and rings: Let (R,m) be a Noetherian local ring and let M be a nonzero finite R-module. The module M is Cohen--Macaulay when depth(M)=dimSuppR(M). The zero module is excluded from this local definition. The local ring R is Cohen--Macaulay when it is Cohen--Macaulay as an R-module.

[F5]

Regular Sequence On A Module: Let R be a commutative unital ring, let M be an R-module, and let x=(x1,,xn) be a finite ordered sequence in R. The sequence is M-regular when M/(x1,,xi1)M0 and multiplication by xi is injective on it for every i, and M/(x)M0.

[F6]

Depth is bounded by support dimension: For every nonzero finite module M over a Noetherian local ring R, 0depthR(M)dimSuppR(M). The nonzero hypothesis is essential for this formulation: under the adopted convention depthR(0)=+, whereas the empty support has no nonnegative Krull dimension.

[F7]

Depth with respect to an ideal: For a finite module M with IMM, depthI(M) is the supremum of the lengths of M-regular sequences in I; for a local ring depth means depth with respect to its maximal ideal.

Proof

1.1

The ring is a domain. Successively apply the parameter-quotient lemma: after c quotients the remaining cotangent classes form a basis, and the quotient is regular of dimension dc. This starts with c=0 and ends with R/m=k0.

F1F3
2.1

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 d, and the depth definition therefore gives depthRd; the support-dimension bound gives depthRd. Thus the Cohen–Macaulay definition holds. For d=0, the empty tuple and the field R give the same conclusion.

F2F4F5F6F7step 1.1

Depends on

Used by

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