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.
The symbolic-power step inside the principal ideal theorem
Statement
Let be a Noetherian local domain, and let be nonzero. If is minimal over , then every prime ideal strictly contained in is zero. In particular .
Facts & Assumptions
Given: A Noetherian local domain and a nonzero element such that is minimal over .
In a domain, the zero ideal is prime (Zero divisor, and integral domain: a commutative ring with and no zero divisors, Prime ideals and maximal ideals in a commutative ring).
Quotients and localizations of Noetherian rings are Noetherian, and every ideal of a Noetherian ring is finitely generated (Every quotient and every localisation of a Noetherian ring is Noetherian, A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member).
The nilradical of a Noetherian ring is nilpotent (The nilradical of a Noetherian ring is nilpotent).
Prime ideals of a localization correspond to primes disjoint from its denominator set (Prime ideals of a localization are exactly the primes disjoint from the denominator set).
If for a finitely generated module, then for some (Determinant trick for Nakayama).
In a local ring, every element outside the unique maximal ideal is a unit; in particular is a unit for in the maximal ideal (Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of and is a unit for every ).
Proof
Since is both maximal and minimal among primes containing , it is the only such prime. Hence the quotient is Noetherian by [L2] and has the single prime . Its nilradical is therefore , so [L3] gives for some . Each layer is a finite-dimensional vector space over : it is finitely generated by [L2] and is annihilated by . A descending chain of ideals in induces descending chains in these finitely many finite-dimensional layers, so all layers, and therefore the original chain, stabilize. Thus is Artinian.
Let be prime. Then . For , define the symbolic power These form a descending chain. By step 1.1, the ideals in stabilize, so for some , If , write with . In the element is a unit, while ; hence . Therefore
The quotient module is finitely generated by [L2], and step 2.1 says . Apply [L5] with . It gives for some . Fact [L6] makes a unit, so and . Localizing this equality at gives
Apply [L5] in the local ring to the finite module and the ideal . Step 3.1 says that ideal times the module is the module, so [L6] gives . Because is a domain, this forces , and contraction through [L4] gives . Thus every prime strictly below is zero, and [L1] yields .
Depends on
- Prime ideals and maximal ideals in a commutative ring
- Zero divisor, and integral domain: a commutative ring with $1 \ne 0$ and no zero divisors
- Every quotient and every localisation of a Noetherian ring is Noetherian
- A commutative ring is Noetherian exactly when every ideal is finitely generated, exactly when its ideals satisfy the ascending chain condition, and exactly when every nonempty set of ideals has a maximal member
- The nilradical of a Noetherian ring is nilpotent
- Prime ideals of a localization are exactly the primes disjoint from the denominator set
- Assuming the Axiom of Choice, a nonzero commutative ring is local exactly when its nonunits form an ideal, exactly when one of $x$ and $1-x$ is a unit for every $x$
- Determinant trick for Nakayama
Used by
- Krull's principal ideal theorem Theorem
Dependency tree · two levels
35 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
- J. S. Milne, A Primer of Commutative Algebra, v4.03, §21 (standard reference, not scraped)
- Melvin Hochster, Dimension theory and systems of parameters (standard reference, not scraped)