Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-09-01
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

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: A Noetherian local ring (R,m) with d=dim⁡R>0 and a system of parameters (x,x2,…,xd).

[L1]

The image of (x2,…,xd) in R/(x) is a system of parameters there, equivalently an m/(x)-primary ideal generated by d−1 elements (Systems of parameters and parameter ideals, Parameter ideals are exactly the m-primary d-generated ideals).

[L2]

A prime minimal over an ideal generated by r 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.1

By [L1], the maximal ideal of R/(x) is minimal over an ideal generated by d−1 elements. Applying the height theorem in the quotient ring, and then reading dimension as the height of its maximal ideal, gives dim⁡(R/(x))≤d−1.

L1L2L3given
2.1

Suppose instead that dim⁡(R/(x))≤d−2. Then [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.

L2L3step 1.1
3.1

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

step 1.1step 2.1∎

Depends on

Used by

Dependency tree · two levels

18 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