TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

The Galois translation theorem

Statement

Let $E / F$ be finite Galois and let $L / F$ be a field extension inside a common overfield. Then $E L / L$ is finite Galois, and restriction gives

$Gal (E L / L) ≅ Gal (E / E \cap L) .$

Facts & Assumptions

Given: The compositum $E L$ and intersection $D : = E \cap L$ inside the common overfield.

[L1]

A finite extension is Galois if and only if it is the splitting field of a separable polynomial, and for a finite Galois extension the fixed field of the full Galois group is the base field (Equivalent characterizations of a finite Galois extension).

[L2]

If $H$ is a finite group of automorphisms of a field $K$ , then $[K : K^{H}] = ∣ H ∣$ and $Aut (K / K^{H}) = H$ (Artin's fixed-field theorem: $[K : K^{G}] = ∣ G ∣$ and $Aut (K / K^{G}) = G$ ).

Proof

technique · direct

1.1L1

By [L1], $E$ is the splitting field over $F$ of a separable polynomial $f$ . The same polynomial over $L$ remains separable and has splitting field $E L$ , so [L1] makes $E L / L$ finite Galois.

2.1step 1.1

An element of $Gal (E L / L)$ permutes the roots of $f$ , hence preserves $E$ , and its restriction to $E$ fixes $D = E \cap L$ . Restriction therefore defines a homomorphism into $Gal (E / D)$ ; it is injective because $E L$ is generated by $E$ and $L$ .

3.1step 2.1L1L2∎

Let $H$ be the restriction image. By [L1], an element of $E$ is fixed by $H$ exactly when it is fixed by every automorphism of $E L / L$ , exactly when it lies in $L$ ; thus $E^{H} = E \cap L = D$ . By [L2], $H = Aut (E / E^{H}) = Gal (E / D)$ , so restriction is surjective and hence an isomorphism. If $E \subseteq L$ , both groups are trivial; if $L = F$ or $D = F$ , the displayed formula specializes directly.

Depends on

Used by

Dependency tree · two levels

14 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

J. S. Milne, Fields and Galois Theory, v5.10, Proposition 3.19 (standard reference, not scraped)