TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 group of a compositum is a fibre product of Galois groups

Statement

Let $E_{1} / F$ and $E_{2} / F$ be finite Galois extensions inside a common overfield, and put $D = E_{1} \cap E_{2}$ . Then $E_{1} E_{2} / F$ is finite Galois and restriction identifies its Galois group with the fibre product

${(σ_{1}, σ_{2}) \in Gal (E_{1} / F) \times Gal (E_{2} / F) : σ_{1} ∣_{D} = σ_{2} ∣_{D}} .$

This image is the full direct product exactly when $D = F$ .

Facts & Assumptions

Given: Finite Galois extensions $E_{1} / F$ and $E_{2} / F$ ; writing $f_{i}$ for a separable polynomial with splitting field $E_{i}$ , their compositum is the splitting field over $F$ of the product of the distinct irreducible factors of $f_{1} f_{2}$ , a polynomial with the same roots as $f_{1} f_{2}$ and no repeated one, so the compositum is Galois by Equivalent characterizations of a finite Galois extension; restriction from a Galois extension onto a Galois intermediate field is surjective by Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence; and the fixed field of a full finite Galois group is the base field by The fundamental theorem of finite Galois theory.

[L1]

For finite Galois $E / L_{0}$ and any extension $L / L_{0}$ , restriction gives $Gal (E L / L) ≅ Gal (E / E \cap L)$ (The Galois translation theorem).

Proof

technique · direct

1.1

Restriction sends $Gal (E_{1} E_{2} / F)$ injectively into the product of the two relative Galois groups, since $E_{1} E_{2}$ is generated by $E_{1}$ and $E_{2}$ . Both restrictions agree on $D$ , so the image lies in the displayed fibre product.

given

2.1

Conversely, let $(σ_{1}, σ_{2})$ have equal restrictions to $D$ . Extend $σ_{2}$ to some $τ \in Gal (E_{1} E_{2} / F)$ using surjectivity of restriction. Then $ρ : = σ_{1} (τ ∣_{E_{1}})^{- 1}$ fixes $D$ , and [L1] supplies $h \in Gal (E_{1} E_{2} / E_{2})$ with $h ∣_{E_{1}} = ρ$ . The automorphism $h τ$ restricts to $σ_{1}$ and $σ_{2}$ , proving that every compatible pair is in the image.

step 1.1L1given

3.1

For the forward implication of the last assertion, if $D = F$ then compatibility is automatic and step 2.1 gives the full product. For the reverse implication, if the image is the full product, every pair $(1, σ_{2})$ is compatible, so every $σ_{2} \in Gal (E_{2} / F)$ fixes $D$ ; its fixed field is $F$ , hence $D = F$ . If $E_{1} = E_{2}$ , the fibre product is instead the diagonal subgroup, as the formula requires.

step 2.1given∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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.21 (standard reference, not scraped)