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.
Choose the first generator's minimal prime inside the target prime
Statement
Let be a Noetherian commutative ring, let , let
and let be a prime ideal minimal over . Let be the minimal prime ideals over . If is not one of the and if
is a strict prime chain, then there exists a strict prime chain of the same length ending at whose first proper subprime is not contained in any . For such a chain one can choose
and then is minimal over .
Facts & Assumptions
Given: A Noetherian commutative ring , an integer , the ideal , a prime ideal minimal over , the minimal primes over , and a strict chain .
A Noetherian ring has finitely many minimal primes over any ideal (A Noetherian ring has finitely many minimal prime ideals, Minimal primes over a proper ideal exist).
Finite prime avoidance lets us choose an element outside a finite union of prime ideals once the ambient ideal is not contained in that union (An ideal contained in a finite union of prime ideals lies in one of them).
Every prime minimal over a principal ideal has height at most (Krull's principal ideal theorem).
Proof
By [L1], the family is finite. Repeatedly applying the two-step prime-avoidance argument to the triples for produces a strict chain of the same length ending at whose first proper subprime is not contained in any . Relabel so that the resulting chain is again with for every .
Since is not contained in the finite union , [L2] gives . In particular , so contains .
Let be prime minimal over . Because contains , it contains one of the minimal primes . By the choice of , one has , so . If , then is a strict chain in the quotient ring , so the prime has height at least . But is minimal over , hence is minimal over the principal ideal generated by the image of , contradicting [L3]. Therefore .
Hence is minimal over , with chosen from the first proper subprime of a chain of the same length.
Depends on
Used by
Dependency tree · two levels
12 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)
- The Stacks Project, Section 10.60: Dimension (standard reference, not scraped)