Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 τ:EE be a field isomorphism carrying a subfield FE onto FE, and write σ=τF. Then σ:F[x]F[x],iaixiiσ(ai)xi is a ring isomorphism, and for every fF[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 τ:EE with τ(F)=F and restriction σ:FF.

[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 xF[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 · 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