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.
Krull's principal ideal theorem
Statement
Assume the Axiom of Choice (The Axiom of Choice). Let be a Noetherian commutative ring, let , and let be a prime ideal minimal over . Then .
Facts & Assumptions
Given: The Axiom of Choice, a Noetherian commutative ring , an element , and a prime ideal minimal over .
The principal-ideal bound reduces to the case of a Noetherian local domain whose maximal ideal is minimal over one nonzero element (Reduce the principal ideal theorem to a Noetherian local domain).
Under the assumed AC, in that reduced local-domain situation every prime properly below the maximal ideal is zero, so the maximal ideal has height at most (The symbolic-power step inside the principal ideal theorem).
Proof
By [L1], choose a minimal prime and pass to the Noetherian local domain whose maximal ideal is minimal over the image of .
Fact [L2] applies to , so its maximal ideal has height at most .
The reduction packaged in [L1] identifies this with the desired bound upstairs in .
Depends on
Used by
- A minimal prime over a principal nonzerodivisor has height one Corollary
- The genus of a smooth plane curve in terms of its degree Corollary
- A normal singular surface: the quadric cone Counterexample
- A Weil divisor that is not Cartier at the vertex of the quadric cone Counterexample
- The intersection product needs Cartier or complementary-dimension hypotheses Counterexample
- The Riemann inequality is not an equality for special divisors Counterexample
- Choose the first generator's minimal prime inside the target prime Lemma
- Depth is bounded by the quotient dimension at every associated prime Lemma
- Finite local length exactly when no common local branch Lemma
- Reduced Cartier multiples on a normal local surface Lemma
- Select generators witnessing the converse height theorem Lemma
- Strict henselization of a DVR and smooth sections Lemma
- The trace discriminant detects étaleness of a finite free algebra Lemma
- A nontrivial principal section has pure codimension one Theorem
- Krull's height theorem Theorem
- Regular local rings are unique factorization domains Theorem
- Rosenlicht dichotomy for smooth connected algebraic groups Theorem
- Weil's extension theorem for rational maps into smooth separated group schemes Theorem
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
- Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., §21 (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §21 (standard reference, not scraped)
- The Stacks Project, Section 10.60: Dimension (standard reference, not scraped)