Alphabeta MathHow 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.
dimension at most embedding dimension
Statement
Assume the Axiom of Choice.
Every nonzero commutative Noetherian local ring satisfies .
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.
embedding dimension is minimal maximal ideal generator number: For a nonzero Noetherian local ring , is the least number of generators of .
Krull's height theorem: Under the Axiom of Choice, if is minimal over an ideal generated by elements in a Noetherian ring, then .
Proof
Let . The maximal ideal has a generating tuple of length . If , it is zero; then every nonzero element is a unit and is a field of dimension zero.
If , the maximal ideal is minimal over itself, so its height is at most by the height theorem. Every prime chain in a local ring can be extended to end at its maximal ideal; hence .
Depends on
Used by
- A flat family with a nodal special fibre is not smooth at the node Counterexample
- betti numbers residue field regular ring Example
- completion regularity invariance Example
- cusp local ring not regular Example
- formal power series ring regular Example
- localised polynomial ring regular Example
- A point blowup lowers pairwise contact order by one and separates transverse branches Lemma
- Blowing up a multiple point separates pairwise transverse components Lemma
- Complex algebraic boundary points admit normalized curve arcs Lemma
- Free differentials imply regularity in characteristic zero Lemma
- Normality of the symmetric determinantal ring Lemma
- regular local quotient by parameter is regular Lemma
- Surjective orbit tangents give finitely many open orbits Lemma
- Point blowups of regular surfaces stay regular, with rational exceptional fibre over the residue field Theorem
- quotient and lifting regularity across a regular element Theorem
- serre normality criterion Theorem
- Tangent dimension bounds local dimension Theorem
Dependency tree · two levels
10 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
- Remark 12.4, p.115 (standard reference, not scraped)