Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-09-24 (gpt-6-sol)
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.

A first parameter lowers local dimension by exactly one

Statement

Assume the Axiom of Choice.

Let (R,m) be a Noetherian local ring of positive dimension d, and let (x,x2,…,xd) be a system of parameters. Then dim⁡(R/(x))=d−1.

Facts & Assumptions

Given: The Axiom of Choice, a Noetherian local ring (R,m) with d=dim⁡R>0, and a system of parameters (x,x2,…,xd).

[L1]

Since (x,x2,…,xd) is a system of parameters, its ideal is m-primary. Hence the images of x2,…,xd generate an m/(x)-primary ideal in R/(x); no dimension of the quotient is assumed here (Systems of parameters and parameter ideals, Parameter ideals are exactly the m-primary d-generated ideals).

[L2]

Under the Axiom of Choice, a prime minimal over an ideal generated by r≥1 elements has height at most r, and conversely a prime of finite height r is locally minimal over r generators (Krull's height theorem, Converse to Krull's height theorem in localised form).

[L3]

Prime ideals of R/(x) correspond to prime ideals of R that contain (x) (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal).

Proof

technique · direct
1.1L1L2L3given

By [L1], the maximal ideal of R/(x) is minimal over an ideal generated by d−1 elements. If d=1, that ideal is zero, so the maximal ideal is a minimal prime and the quotient has dimension zero. If d≥2, apply the height theorem to its d−1≥1 generators. In either case dim⁡(R/(x))≤d−1.

2.1L2L3step 1.1

Suppose instead that dim⁡(R/(x))≤d−2. The quotient is a nonzero local ring, so this is impossible when d=1. For d≥2, [L2] applied in the local ring R/(x) provides an ideal generated by at most d−2 elements whose radical is the maximal ideal m/(x). Lifting those generators to R and adjoining x, we obtain an ideal of R generated by at most d−1 elements with radical m. Applying the height theorem to the maximal ideal of R would then give d=dim⁡R≤d−1, contradiction.

3.1step 1.1step 2.1∎

Therefore dim⁡(R/(x))=d−1.

Depends on

Used by

Dependency tree · two levels

20 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