Separable Extension

Statement

A polynomial $f \in F[x]$ is separable if it has no repeated roots in any extension of $F$, equivalently if $\gcd(f, f') = 1$ where $f'$ is the formal derivative. An algebraic element $\alpha$ over $F$ is separable if its minimal polynomial $\min_F(\alpha)$ is separable. An extension $K/F$ is separable if every $\alpha \in K$ is separable over $F$.

In Mathlib:

• Polynomial.Separable f — the polynomial predicate
• IsSeparable F x — the element predicate (minpoly F x is separable)
• Algebra.IsSeparable F K — the extension predicate

Key fact: Every algebraic extension in characteristic 0 is separable. Specifically, if $F$ has characteristic 0 and $K/F$ is algebraic and integral, then Algebra.IsSeparable F K holds automatically.

Visualization

Separable example — $x^2 - 2 \in \mathbb{Q}[x]$:

Roots $\pm\sqrt{2}$ are distinct. The extension $\mathbb{Q}(\sqrt{2})/\mathbb{Q}$ is separable.

Inseparable example — $x^p - t \in \mathbb{F}_p(t)[x]$ (char $p$ field):

So $\gcd(f, f') = f \ne 1$. The unique root $\alpha = t^{1/p}$ has multiplicity $p$:

This single root is repeated $p$ times — the extension is purely inseparable.

Polynomial	Field	$f'$	$\gcd(f,f')$	Separable?
$x^2 - 2$	$\mathbb{Q}$	$2x$	$1$	Yes
$x^2 + 1$	$\mathbb{Q}$	$2x$	$1$	Yes
$x^p - t$	$\mathbb{F}_p(t)$	$0$	$f$	No
$x^p - x$	$\mathbb{F}_p$	$-1$	$1$	Yes

Proof Sketch

1. Char 0 implies separable. In characteristic 0 the derivative of a non-constant polynomial is non-zero and has strictly smaller degree. An irreducible $f$ and $f'$ cannot share a factor (since $f$ is irreducible and $\deg f' < \deg f$), so $\gcd(f, f') = 1$.
2. Char $p$ inseparability. If $f'= 0$ in char $p$, then $f = g(x^p)$ for some $g$. Expanding $g(x^p) = g(x)^p$ (by the Frobenius endomorphism) shows every root has multiplicity divisible by $p$.
3. Extension perspective. $K/F$ is separable iff the number of $F$-embeddings $K \to \overline{F}$ equals $[K:F]$, i.e., distinct embeddings correspond to distinct roots.

Connections

Separability is one of the two conditions (the other being normality) for a Normal ExtensionNormal Extension$$K/F \text{ normal} \iff \forall f \in F[x],\; f \text{ irred., has a root in } K \implies f \text{ splits in } K$$A field extension where every irreducible polynomial with one root in the extension splits completelyRead more → to be Galois. The Primitive Element Theorem (Primitive Element TheoremPrimitive Element Theorem$$K = F(\theta) \text{ for some } \theta \in K \quad (K/F \text{ finite separable})$$Every finite separable field extension is generated by a single elementRead more →) holds precisely for finite separable extensions.

/-- In characteristic 0 every irreducible polynomial is separable.
    We derive: any integral algebraic extension of a char-0 field is separable. -/
theorem integral_charZero_isSeparable
    (F K : Type*) [Field F] [CharZero F] [Field K] [Algebra F K]
    [Algebra.IsIntegral F K] : Algebra.IsSeparable F K :=
  Algebra.IsSeparable.of_integral