Fundamental Theorem of Galois Theory

Statement

Let $K/F$ be a finite Galois extension with Galois group $G = \text{Gal}(K/F)$. There is an inclusion-reversing bijection:

given by $E \mapsto \text{Gal}(K/E)$ and $H \mapsto K^H$ (the fixed field of $H$).

Moreover:

• $[K:E] = |H|$ and $[E:F] = [G:H]$
• $E/F$ is normal (Galois) if and only if $H$ is a normal subgroup of $G$
• When $E/F$ is Galois, $\text{Gal}(E/F) \cong G/H$

Example: Splitting Field of $x^4 - 2$

The splitting field of $x^4 - 2$ over $\mathbb{Q}$ is $\mathbb{Q}(\sqrt[4]{2}, i)$. The Galois group is the dihedral group $D_4$ of order 8. The lattice of subgroups of $D_4$ corresponds precisely to the lattice of intermediate fields.

Connections

This theorem underlies the proof of the Impossibility of the Quintic FormulaImpossibility of the Quintic Formula$$S_5 \text{ is not solvable} \implies \text{no radical formula for degree } \geq 5$$No general algebraic formula exists for polynomials of degree 5 or higherRead more →. It also explains the result on Constructible NumbersConstructible Numbers$$\text{Regular } n\text{-gon constructible} \iff n = 2^a \cdot p_1 \cdot p_2 \cdots p_k$$Which regular n-gons can be constructed with compass and straightedge?Read more → (regular $n$-gon constructibility reduces to checking whether the Galois group has a composition series with all factors of order 2).

/-- The Galois correspondence as an order-reversing bijection between
    intermediate fields and subgroups of the Galois group. Mathlib
    packages the Fundamental Theorem as the order isomorphism
    `IntermediateField F K ≃o (Subgroup (K ≃ₐ[F] K))ᵒᵈ`, where the
    `ᵒᵈ` (order dual) captures the inclusion-reversing direction. -/
noncomputable def galois_correspondence
    (F K : Type*) [Field F] [Field K] [Algebra F K]
    [FiniteDimensional F K] [IsGalois F K] :
    IntermediateField F K ≃o (Subgroup (K ≃ₐ[F] K))ᵒᵈ :=
  IsGalois.intermediateFieldEquivSubgroup