Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-13
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 τ:E→E′ be a field isomorphism carrying a subfield F⊆E onto F′⊆E′, and write σ=τ∣F. Then σ∗:F[x]⟶F′[x],∑iaixi⟼∑iσ(ai)xi is a ring isomorphism, and for every f∈F[x] and α∈E, τ(f(α))=(σ∗f)(τ(α)). Consequently τ carries roots of f bijectively to roots of σ∗f, transports factorizations coefficientwise, and carries a splitting field of f over F to a splitting field of σ∗f over F′.

Facts & Assumptions

Given: An isomorphism τ:E→E′ with τ(F)=F′ and restriction σ:F→F′.

[F1]

A coefficient homomorphism and the chosen image of x determine a unique homomorphism of polynomial rings (Universal property of R[x]: a coefficient homomorphism and the image of x determine a unique ring homomorphism).

[F2]

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).

[F3]

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

technique · direct
1.1

Apply [F1] to σ and the indeterminate x∈F′[x]. This gives σ∗ with the displayed coefficient formula. Applying the same construction to σ−1 gives its inverse, so σ∗ is an isomorphism.

F1
1.2

For f=∑iaixi, the homomorphism laws give τ(f(α))=∑iσ(ai)τ(α)i=(σ∗f)(τ(α)). Thus f(α)=0 if and only if (σ∗f)(τ(α))=0, because τ is injective.

F2algebra
2.1

Applying the construction of step 1.1 to τ gives a coefficientwise isomorphism τ∗:E[x]→E′[x] extending σ∗. It transports every product factorisation and, in particular, a linear factorisation of f to one of σ∗f. Since τ is bijective, step 1.2 gives a bijection of root sets, and τ(F(roots of f))=F′(roots of σ∗f). The splitting-field claim follows from [F3].

F1F3step 1.1step 1.2∎

Depends on

Used by

Dependency tree · two levels

13 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