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.
An integral domain extension can fail going down when the base is not normal
Example
Let be a field, let
let
and let
Then is an integral extension of domains, is a strict prime chain in , lies over , and there is no prime ideal of lying over . So going down fails although both rings are domains.
Facts & Assumptions
Given: A field , the rings , the ideals in , and the prime in .
Assuming the Axiom of Choice, going down holds for integral extensions over integrally closed domains (Going down holds for integral extensions over integrally closed domains).
Verification
The ring is a domain, and is a subring of it, so is also a domain. Moreover satisfies the monic equation with coefficient , and because already. Hence is integral over .
The ideals and are prime because they are contractions of the prime ideals and of , and they are distinct because . The ideal is prime in , and its contraction to is , since mod one has and , so , , and all vanish.
The base ring is not integrally closed: the element is integral over by step 1.1, but . Indeed, if , then setting would express as a polynomial in ; evaluating at and would then give the same value on both inputs, impossible because takes the values and .
Suppose were a prime ideal of with . Because does not contain , neither does . But and , so primality of and force and . Hence , and therefore . This contradicts because step 2.1 showed .
Thus the integral extension of domains has a prime chain and a prime over with no prime below lying over . So the normality hypothesis in [L1] is essential.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 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
- Melvin Hochster, Introduction to Commutative Algebra, Chapter 3, lecture of September 30 (standard reference, not scraped)