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.
A field isomorphism transports polynomials coefficientwise and carries roots, factorizations, and splitting to roots, factorizations, and splitting
Statement
Let be a field isomorphism carrying a subfield onto , and write . Then is a ring isomorphism, and for every and , Consequently carries roots of bijectively to roots of , transports factorizations coefficientwise, and carries a splitting field of over to a splitting field of over .
Facts & Assumptions
Given: An isomorphism with and restriction .
A coefficient homomorphism and the chosen image of determine a unique homomorphism of polynomial rings (Universal property of : a coefficient homomorphism and the image of determine a unique ring homomorphism).
Polynomial evaluation is substitution into the coefficient sum, and a root is an element where that evaluation is zero (Evaluation and roots of a polynomial in a commutative target ring).
A splitting field is generated over the base by all roots of a polynomial that splits there (Polynomials that split and splitting fields of a polynomial or a family of polynomials).
Proof
Apply [F1] to and the indeterminate . This gives with the displayed coefficient formula. Applying the same construction to gives its inverse, so is an isomorphism.
For , the homomorphism laws give . Thus if and only if , because is injective.
Applying the construction of step 1.1 to gives a coefficientwise isomorphism extending . It transports every product factorisation and, in particular, a linear factorisation of to one of . Since is bijective, step 1.2 gives a bijection of root sets, and . The splitting-field claim follows from [F3].
Depends on
Used by
- A base-field isomorphism extends across simple adjunctions of corresponding roots of an irreducible polynomial Lemma
- Every F-endomorphism of a splitting field permutes the distinct roots and is an automorphism Proposition
- A base-field isomorphism extends to an isomorphism between splitting fields of corresponding polynomials Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 26 results over 8 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- T. Judson, Abstract Algebra: Theory and Applications, Section 21.2 (standard reference, not scraped)