PropositionStatement: 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.

Every $F$ -endomorphism of a splitting field permutes the distinct roots and is an automorphism

Statement

Let $E / F$ be a splitting field of a nonzero polynomial $f \in F [x]$ . Every field homomorphism $τ : E \to E$ that fixes $F$ maps the finite set of distinct roots of $f$ bijectively to itself. Consequently $τ$ is surjective and hence is an $F$ -automorphism of $E$ .

Facts & Assumptions

Given: A splitting field $E / F$ of $0 \neq f \in F [x]$ and an $F$ -endomorphism $τ : E \to E$ .

[F1]

A unital homomorphism between fields is injective (Field homomorphism and embedding).

[F2]

A field isomorphism carries roots of a polynomial to roots of the transported polynomial (A field isomorphism transports polynomials coefficientwise and carries roots, factorizations, and splitting to roots, factorizations, and splitting).

[F3]

A nonzero degree- $n$ polynomial over a domain has at most $n$ distinct roots (A nonzero polynomial of degree $n$ over an integral domain has at most $n$ distinct roots).

[F4]

An injection from a finite set to itself is a bijection (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ ).

[F5]

A splitting field is generated over the base field by the roots of its polynomial (Polynomials that split and splitting fields of a polynomial or a family of polynomials).

Proof

technique · direct

1.1

By [F1], $τ$ is injective and hence an isomorphism from $E$ onto its image. Since it fixes the coefficients of $f$ , direct evaluation gives $f (τ (α)) = τ (f (α)) = 0$ for every root $α$ of $f$ .

F1F2

2.1

The distinct-root set $X$ is finite by [F3], and step 1.1 restricts $τ$ to an injection $X \to X$ . By [F4], this restriction is a bijection, so $τ$ permutes the roots. This remains true when $X$ is empty.

F3F4step 1.1

3.1

The image $τ (E)$ contains $F$ and every root of $f$ by step 2.1. Since those elements generate $E$ by [F5], one has $E \subseteq τ (E) \subseteq E$ . Thus $τ$ is surjective and is an $F$ -automorphism.

F5step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 59 results over 17 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

J. S. Milne, Fields and Galois Theory, Chapter 2 (standard reference, not scraped)

Every FF-endomorphism of a splitting field permutes the distinct roots and is an automorphism