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.
Lying over for integral ring maps
Statement
Assume the Axiom of Choice.
Let be an integral ring map, and let with . Then there exists a prime ideal such that .
Facts & Assumptions
Given: An integral ring map and a prime ideal containing .
Integral ring maps are exactly those whose target elements satisfy monic equations over the source ring (Integral ring maps and integral extensions).
Integrality is preserved by localisation (Integrality and integral closure commute with localisation).
In an integral extension, a prime upstairs is maximal exactly when its contraction is maximal (Under an integral extension, a prime is maximal if and only if its contraction is maximal).
The quotient by a prime ideal is a domain ( is an integral domain if and only if is a prime ideal).
Prime ideals of a quotient correspond exactly to primes containing the kernel ideal (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal).
Prime ideals of a localisation correspond exactly to primes disjoint from the denominator set (Prime ideals of a localization are exactly the primes disjoint from the denominator set).
Assuming the Axiom of Choice, every proper ideal of a nonzero commutative ring is contained in a maximal ideal (In a nonzero commutative ring, every proper ideal is contained in a maximal ideal).
A localisation is the zero ring exactly when belongs to the denominator set (Equality, vanishing, and the kernel of the localisation map).
Proof
Let , let be the quotient map, and let . By [L6], prime ideals of correspond to prime ideals of containing , so is prime. The map factors through an injective integral map , so it is enough to find a prime of contracting to and then pull it back through [L6].
Replace by and write again for the chosen prime. Set . By [L5], is a domain, so contains no zero element of ; since is injective, inside as well. Hence [L9] shows that is nonzero. By [L2], the map is integral.
By [L7], prime ideals of correspond to prime ideals of contained in . Therefore every prime of lies inside , so is the unique maximal ideal of . By [L8], the nonzero ring has a maximal ideal . Then [L3] implies that .
By [L7], the prime ideal of is for a unique prime ideal of disjoint from , and its contraction to is the contraction of , namely . Therefore lies over . Pulling back through step 1.1 gives a prime of lying over the original prime of .
Depends on
- Integral ring maps and integral extensions
- Integrality and integral closure commute with localisation
- Under an integral extension, a prime is maximal if and only if its contraction is maximal
- $\operatorname{Frac}(D)$ is a field and $d\mapsto d/1$ embeds the integral domain $D$
- $R/P$ is an integral domain if and only if $P$ is a prime ideal
- Prime ideals of a quotient ring are exactly the prime ideals containing the ideal
- Prime ideals of a localization are exactly the primes disjoint from the denominator set
- In a nonzero commutative ring, every proper ideal is contained in a maximal ideal
- Equality, vanishing, and the kernel of the localisation map
Used by
Dependency tree · two levels
31 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., Theorem (14.3)(3) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Proposition 7.5 (standard reference, not scraped)