Alphabeta Math
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.

Normal subgroups, conjugate fields, and quotient groups in the Galois correspondence

Statement

Let K/F be finite Galois, let G=Gal⁡(K/F), let H≤G, and put E=KH. For every σ∈G,

Gal⁡(K/σ(E))=σHσ−1.

An intermediate field E/F is Galois exactly when its corresponding subgroup is normal. In that case restriction gives a surjective homomorphism G→Gal⁡(E/F) with kernel H, and hence

Gal⁡(E/F)≅G/H.

Facts & Assumptions

Given: The finite Galois correspondence; normal subgroups and quotient groups (Normal subgroup: invariance under conjugation, The quotient group G/N and coset product (gN)(hN)=ghN); the characterization of a normal algebraic extension by stability of conjugates (A normal algebraic extension is one in which every minimal polynomial with a root in the extension splits there); the Axiom of Choice and algebraic embedding extension (Assuming Choice, a base-field embedding extends across every algebraic extension); and the first isomorphism theorem for groups (First isomorphism theorem for groups: G/ker⁡f≅im⁡f).

[L1]

The assignments H↦KH and E↦Gal⁡(K/E) are mutually inverse inclusion-reversing bijections (The fundamental theorem of finite Galois theory).

[F1]

A subgroup is normal exactly when it is invariant under conjugation (Equivalent characterisations of a normal subgroup by conjugates and left and right cosets).

Proof

technique · direct
1.1L1algebra

For x∈K, the element x is fixed by σHσ−1 exactly when σ−1(x) is fixed by H, exactly when σ−1(x)∈E, and exactly when x∈σ(E). Thus KσHσ−1=σ(E), and [L1] gives Gal⁡(K/σ(E))=σHσ−1.

2.1step 1.1L1F1given

For the forward direction, if H⊴G, then step 1.1 gives σ(E)=E for every σ∈G; every F-conjugate of an element of E is obtained by extending its embedding to K and hence lies in E, so E/F is normal, and it is separable as a subextension of the separable extension K/F, hence Galois. For the reverse direction, if E/F is Galois, normality gives σ(E)=E for every σ∈G, so step 1.1 and [L1] give σHσ−1=H and [F1] gives H⊴G.

3.1step 2.1L1given∎

In the normal case, restriction ρ:G→Gal⁡(E/F) is defined by step 2.1. Every F-automorphism of E extends to an embedding of K in an algebraic closure; normality of K/F makes the extension an element of G, so ρ is surjective. Its kernel consists exactly of the automorphisms fixing E, namely H by [L1]. The first isomorphism theorem therefore gives G/H≅Gal⁡(E/F); for H={1} and H=G this yields the two endpoint quotients.

Depends on

Used by

Dependency tree · two levels

30 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