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.
Minimal polynomials of integral elements over an integrally closed domain have coefficients in the domain
Statement
Let be an integrally closed domain with field of fractions , let be a field extension, and let be integral over . Then the minimal polynomial of over has coefficients in .
In particular, if is monic and factors in as
with , then .
Facts & Assumptions
Given: An integrally closed domain with field of fractions , a field extension , and an element integral over .
The phrase "integrally closed domain" means that every element of integral over already lies in (Integral closure in an extension ring and integrally closed domains).
Integral elements over a nonzero base ring form a subring (Integral elements over a nonzero base ring form a subring).
An algebraic element over a field has a unique monic irreducible minimal polynomial, and it divides every polynomial that vanishes at that element (The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element).
Every nonzero polynomial over a field has a splitting field (Every nonzero polynomial over a field has a splitting field).
If a monic irreducible polynomial over a field has two roots in extensions, there is a field homomorphism between the simple extensions sending one root to the other (Universal property of adjoining a root of an irreducible polynomial).
Proof
By [L3], the minimal polynomial of is monic and irreducible. Since is integral over , it satisfies some monic polynomial in , so [L3] implies that is nonzero. By [L4], choose a splitting field for and write with .
Let be a monic polynomial with . For each root of , the universal property [L5] gives a -homomorphism sending to . Applying that homomorphism to the identity shows . Thus every is integral over .
The coefficients of are, up to sign, the elementary symmetric polynomials in the integral elements . Since is a domain and therefore nonzero, [L2] shows that these symmetric polynomials are integral over . But the coefficients also lie in , so [L1] forces them to lie in . This proves the first statement.
For the factor statement, choose a splitting field of over and write . Each is integral over because it is a root of the monic polynomial . Therefore the coefficients of are integral over by the same symmetric-polynomial argument as in step 3.1, and they lie in because . Hence [L1] forces all coefficients of to lie in .
Depends on
- Integral closure in an extension ring and integrally closed domains
- Integral elements over a nonzero base ring form a subring
- The evaluation kernel and the unique monic irreducible minimal polynomial of an algebraic element
- Every nonzero polynomial over a field has a splitting field
- Universal property of adjoining a root of an irreducible polynomial
Used by
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., Proposition (14.8) (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Proposition 6.11 (standard reference, not scraped)