Primitive Element Theorem

Statement

Let $K/F$ be a finite separable field extension. Then there exists a primitive element $\theta \in K$ such that $K = F(\theta)$.

Equivalently, $K$ is a simple extension: there is a single algebraic element whose adjunction to $F$ recovers all of $K$.

In Mathlib: Field.exists_primitive_element states this for [FiniteDimensional F K] and [Algebra.IsSeparable F K].

Visualization

Example: $\mathbb{Q}(\sqrt{2}, \sqrt{3})$ over $\mathbb{Q}$.

The extension has degree 4. We claim $\theta = \sqrt{2} + \sqrt{3}$ is a primitive element.

Step 1 — compute powers of $\theta$:

$n$	$\theta^n$
$0$	$1$
$1$	$\sqrt{2} + \sqrt{3}$
$2$	$5 + 2\sqrt{6}$
$3$	$11\sqrt{2} + 9\sqrt{3}$

Step 2 — the minimal polynomial of $\theta = \sqrt{2} + \sqrt{3}$ over $\mathbb{Q}$:

So $\min_\mathbb{Q}(\theta) = x^4 - 10x^2 + 1$, which is irreducible over $\mathbb{Q}$ (it has four distinct real roots $\pm\sqrt{2} \pm \sqrt{3}$, and factors over no quadratic subfield).

Step 3 — since $[\mathbb{Q}(\theta):\mathbb{Q}] = 4 = [\mathbb{Q}(\sqrt{2},\sqrt{3}):\mathbb{Q}]$, we have $\mathbb{Q}(\sqrt{2},\sqrt{3}) = \mathbb{Q}(\sqrt{2}+\sqrt{3})$.

Key roots of $x^4 - 10x^2 + 1$:

Proof Sketch

1. Infinite base field case. If $F$ is infinite, choose $c \in F$ such that $\theta = \alpha + c\beta$ is a primitive element for $K = F(\alpha, \beta)$ (two-element case). The set of "bad" values of $c$ (where $F(\alpha + c\beta) \subsetneq K$) is finite — it equals the set of ratios $(\sigma(\alpha) - \alpha)/(\beta - \sigma(\beta))$ for automorphisms $\sigma$ fixing $\alpha + c\beta$ but not $\beta$. Since $F$ is infinite, a good $c$ exists.
2. Finite base field case. The multiplicative group $K^\times$ of a finite field is cyclic; any generator is a primitive element.
3. Induction. Apply the two-generator case repeatedly to handle $K = F(\alpha_1, \ldots, \alpha_n)$.

Connections

The Primitive Element Theorem is used in the proof of the Fundamental Theorem of Galois TheoryFundamental Theorem of Galois Theory$$\{\text{intermediate fields}\} \longleftrightarrow \{\text{subgroups of } \text{Gal}(K/F)\}$$Bijection between intermediate fields and subgroups of the Galois groupRead more → to ensure Galois extensions are simple. It also appears in the study of 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 →: the tower of quadratic extensions used to characterize constructibility consists of successive simple extensions.

/-- Primitive Element Theorem: a finite separable extension has a single generator. -/
theorem primitive_element (F K : Type*) [Field F] [Field K] [Algebra F K]
    [FiniteDimensional F K] [Algebra.IsSeparable F K] :
    ∃ θ : K, F⟮θ⟯ = ⊤ :=
  Field.exists_primitive_element F K