[proofplan] We prove the four characterisations are equivalent by establishing a cycle of implications: (1) $\Rightarrow$ (2) $\Rightarrow$ (3) $\Rightarrow$ (1), and separately (1) $\Leftrightarrow$ (4). The key ingredients are the [Bound on Automorphisms](/theorems/1255), the [Characterisation of Separable Extensions](/theorems/1265), the fact that [Normal Equals Splitting Field](/theorems/1269), and the [Galois Criterion via Fixed Fields](/theorems/1273). The implication (3) $\Rightarrow$ (1) uses the counting argument from [Splitting Fields of Separable Polynomials Are Galois](/theorems/1271). [/proofplan]

[step:Show (1) $\Rightarrow$ (2): a Galois extension is normal and separable]Let $G = \operatorname{Gal}(K/k)$ and assume $|G| = [K : k]$. We must show $K/k$ is both normal and separable. **Separability.** Let $\alpha \in K$ and let $m_{\alpha,k} \in k[x]$ be the minimal polynomial of $\alpha$ over $k$. Each $\sigma \in G$ sends $\alpha$ to a root of $m_{\alpha,k}$ in $K$, and distinct elements of $G$ that differ on $\alpha$ produce distinct roots. Consider the orbit $G \cdot \alpha = \{\sigma(\alpha) : \sigma \in G\}$. The polynomial \begin{align*} g(x) = \prod_{\beta \in G \cdot \alpha} (x - \beta) \in K[x] \end{align*} is fixed by every $\sigma \in G$ (since $G$ permutes $G \cdot \alpha$), so its coefficients lie in $K^G$. We will show $K^G = k$ in the (1) $\Leftrightarrow$ (4) step below; assuming this, $g \in k[x]$. Since $m_{\alpha,k}$ is the minimal polynomial and $m_{\alpha,k}(\alpha) = 0$ with $g(\alpha) = 0$ and $g \in k[x]$, we have $m_{\alpha,k} \mid g$. But $g$ has distinct roots (the elements of $G \cdot \alpha$ are distinct in $K$), so $m_{\alpha,k}$ has no repeated roots. Hence $\alpha$ is separable over $k$. Since $\alpha \in K$ was arbitrary, $K/k$ is separable. **Normality.** By the argument above, $m_{\alpha,k} \mid g$ and all roots of $g$ lie in $K$. Therefore all roots of $m_{\alpha,k}$ lie in $K$. Since $\alpha \in K$ was arbitrary, every irreducible polynomial in $k[x]$ that has a root in $K$ splits completely in $K$, which is the definition of normality.[/step]

[guided]We assume $|\operatorname{Gal}(K/k)| = [K : k]$ and want to show $K/k$ is both normal and separable. The strategy is to use the Galois group to control the roots of minimal polynomials. **Why does the Galois group help with separability?** Each $k$-automorphism $\sigma \in G$ must send any $\alpha \in K$ to a root of its minimal polynomial $m_{\alpha,k}$, because $\sigma$ fixes $k$ pointwise and therefore preserves the relation $m_{\alpha,k}(\alpha) = 0$. The key insight is that distinct automorphisms that differ on $\alpha$ produce distinct roots, so the orbit $G \cdot \alpha = \{\sigma(\alpha) : \sigma \in G\}$ gives us a supply of distinct roots. Define \begin{align*} g(x) = \prod_{\beta \in G \cdot \alpha} (x - \beta) \in K[x]. \end{align*} Every $\sigma \in G$ permutes the set $G \cdot \alpha$ (if $\beta = \tau(\alpha)$, then $\sigma(\beta) = (\sigma \circ \tau)(\alpha) \in G \cdot \alpha$), so $\sigma$ permutes the factors of $g$. Therefore $\sigma(g) = g$ for all $\sigma \in G$, which means the coefficients of $g$ lie in the fixed field $K^G$. We will establish $K^G = k$ independently in the (1) $\Leftrightarrow$ (4) step. Assuming this, $g \in k[x]$. Since $g(\alpha) = 0$ and $m_{\alpha,k}$ is the minimal polynomial of $\alpha$ over $k$, we have $m_{\alpha,k} \mid g$. But $g$ has all distinct roots by construction (the elements of $G \cdot \alpha$ are distinct elements of $K$). Therefore $m_{\alpha,k}$, being a divisor of $g$, also has all distinct roots, so $\alpha$ is separable over $k$. Since $\alpha$ was arbitrary, the extension $K/k$ is separable. **Normality** follows from the same polynomial $g$. Since $m_{\alpha,k} \mid g$ and every root of $g$ lies in $K$ (they are all of the form $\sigma(\alpha) \in K$), every root of $m_{\alpha,k}$ lies in $K$. This holds for every $\alpha \in K$, so every irreducible polynomial in $k[x]$ with a root in $K$ splits completely over $K$. This is exactly the definition of a normal extension.[/guided]

[step:Show (2) $\Rightarrow$ (3): a normal separable extension is a splitting field of a separable polynomial]Assume $K/k$ is normal and separable. By the [Primitive Element Theorem](/theorems/1267), since $K/k$ is finite and separable, there exists $\gamma \in K$ with $K = k(\gamma)$. Let $f = m_{\gamma,k} \in k[x]$ be the minimal polynomial of $\gamma$ over $k$. Since $K/k$ is separable, $\gamma$ is separable over $k$, so $f$ has no repeated roots. Since $K/k$ is normal, every irreducible polynomial in $k[x]$ with a root in $K$ splits completely in $K$. In particular, $f$ has the root $\gamma \in K$, so $f$ splits completely in $K$. Thus $K$ contains a splitting field of $f$ over $k$. Conversely, $K = k(\gamma)$ is generated over $k$ by a single root of $f$, and a splitting field of $f$ over $k$ is the smallest extension in which $f$ splits. Since $f$ splits in $K$ and $K = k(\gamma)$ is contained in any field over $k$ in which $f$ splits (as $\gamma$ is a root of $f$), $K$ is the splitting field of $f$ over $k$. Hence $K$ is the splitting field of the separable polynomial $f \in k[x]$.[/step]

[guided]Assume $K/k$ is both normal and separable. We need to exhibit a separable polynomial $f \in k[x]$ whose splitting field over $k$ is $K$. The [Primitive Element Theorem](/theorems/1267) applies because $K/k$ is a finite separable extension. It guarantees the existence of $\gamma \in K$ with $K = k(\gamma)$. This is the crucial reduction: instead of dealing with multiple generators, we have a single one. Let $f = m_{\gamma,k} \in k[x]$ be the minimal polynomial of $\gamma$ over $k$, with $\deg f = [k(\gamma) : k] = [K : k]$ by the [Structure of Simple Algebraic Extensions](/theorems/1251). Is $f$ separable? Yes: since $K/k$ is separable, every element of $K$ is separable over $k$; in particular $\gamma$ is, so $m_{\gamma,k}$ has no repeated roots. Does $f$ split in $K$? Since $K/k$ is normal, every irreducible polynomial in $k[x]$ that has at least one root in $K$ splits completely in $K$. The polynomial $f$ is irreducible and has the root $\gamma \in K$, so $f$ splits in $K$. Is $K$ the splitting field? We must verify that no proper subfield of $K$ containing $k$ already splits $f$. The splitting field of $f$ over $k$ is the subfield of $K$ generated over $k$ by all roots of $f$; call it $L$. Then $k \subseteq k(\gamma) \subseteq L$ (since $\gamma$ is one of the roots), so $K = k(\gamma) \subseteq L$. But $L \subseteq K$ since all roots of $f$ lie in $K$. Hence $L = K$.[/guided]

[step:Show (3) $\Rightarrow$ (1): the splitting field of a separable polynomial is Galois]Assume $K$ is the splitting field over $k$ of a separable polynomial $f \in k[x]$. We must show $|\operatorname{Gal}(K/k)| = [K : k]$. This is exactly the content of [Splitting Fields of Separable Polynomials Are Galois](/theorems/1271): if $f \in k[x]$ is separable, then its splitting field over $k$ is a Galois extension of $k$, i.e., $|\operatorname{Gal}(K/k)| = [K : k]$.[/step]

[guided]Assume $K$ is the splitting field of a separable polynomial $f \in k[x]$ over $k$. We need $|\operatorname{Gal}(K/k)| = [K : k]$. The result [Splitting Fields of Separable Polynomials Are Galois](/theorems/1271) gives this directly. Let us sketch the idea behind it. Write $f = \prod_{i=1}^n (x - \alpha_i)$ in $K[x]$, where the $\alpha_i$ are the distinct roots (distinct because $f$ is separable). Since $K$ is the splitting field, $K = k(\alpha_1, \ldots, \alpha_n)$. The proof proceeds by induction on $[K : k]$. If $[K : k] = 1$, then $f$ already splits in $k$ and $\operatorname{Gal}(K/k)$ is trivial, so $|\operatorname{Gal}(K/k)| = 1 = [K : k]$. For the inductive step, suppose $[K : k] > 1$. Let $p = m_{\alpha_1, k}$ be the minimal polynomial of $\alpha_1$ over $k$, with $d = \deg p \geq 2$. Since $f$ is separable and $p \mid f$, the polynomial $p$ is also separable. The [Extension of Isomorphisms to Splitting Fields](/theorems/3313) shows that for each root $\beta$ of $p$ in $K$, there is a $k$-isomorphism $k(\alpha_1) \to k(\beta)$ sending $\alpha_1 \mapsto \beta$, and this extends to a $k$-automorphism of $K$ (since $K$ is a splitting field of $f$ over both $k(\alpha_1)$ and $k(\beta)$). This produces $d$ distinct elements of $\operatorname{Gal}(K/k)$. Now $K$ is also the splitting field of $f$ over $k(\alpha_1)$, and $[K : k(\alpha_1)] = [K : k]/d < [K : k]$. By induction, $|\operatorname{Gal}(K/k(\alpha_1))| = [K : k(\alpha_1)]$. Since $\operatorname{Gal}(K/k(\alpha_1)) \leq \operatorname{Gal}(K/k)$ and the $d$ automorphisms above represent distinct cosets, $|\operatorname{Gal}(K/k)| \geq d \cdot [K : k(\alpha_1)] = [K : k]$. Combined with the [Bound on Automorphisms](/theorems/1255) ($|\operatorname{Gal}(K/k)| \leq [K : k]$), we get equality.[/guided]

[step:Show (1) $\Leftrightarrow$ (4): the Galois condition is equivalent to $k$ being the fixed field]This equivalence is the content of the [Galois Criterion via Fixed Fields](/theorems/1273). **(1) $\Rightarrow$ (4).** Assume $|\operatorname{Gal}(K/k)| = [K : k]$. Set $G = \operatorname{Gal}(K/k)$ and $F = K^G = \{a \in K : \sigma(a) = a \text{ for all } \sigma \in G\}$. Since every $\sigma \in G$ fixes $k$ pointwise, $k \subseteq F$. We have $G \leq \operatorname{Aut}_F(K)$, so $|G| \leq |\operatorname{Aut}_F(K)| \leq [K : F]$ by the [Bound on Automorphisms](/theorems/1255). But $[K : F] \leq [K : k]$ since $k \subseteq F$, and $|G| = [K : k]$ by assumption. Therefore $[K : F] = [K : k]$, which forces $[F : k] = 1$ by the [Tower Law](/theorems/1248), hence $F = k$. **(4) $\Rightarrow$ (1).** Assume $K^{\operatorname{Gal}(K/k)} = k$. Set $G = \operatorname{Gal}(K/k)$ and $n = |G|$. For each $\alpha \in K$, the orbit polynomial $g_\alpha(x) = \prod_{\beta \in G \cdot \alpha} (x - \beta)$ has coefficients in $K^G = k$ (as shown in the first step) and has $\alpha$ as a root. Hence $m_{\alpha,k} \mid g_\alpha$ and $\deg m_{\alpha,k} \leq |G \cdot \alpha| \leq |G| = n$. In particular, $[k(\alpha) : k] = \deg m_{\alpha,k} \leq n$ for every $\alpha \in K$. Since $K/k$ is finite, the [Primitive Element Theorem](/theorems/1267) applies (we verify separability below), giving $K = k(\gamma)$ for some $\gamma$, so $[K : k] = [k(\gamma) : k] \leq n = |G|$. We verify separability: $m_{\gamma,k} \mid g_\gamma$ and $g_\gamma$ has distinct roots, so $m_{\gamma,k}$ is separable, hence $K = k(\gamma)$ is a separable extension. The [Primitive Element Theorem](/theorems/1267) thus applies. Combined with the [Bound on Automorphisms](/theorems/1255), $|G| \leq [K : k]$, we obtain $|G| = [K : k]$, i.e., $K/k$ is Galois.[/step]

[guided]We prove both directions of the equivalence between condition (1) ($|\operatorname{Gal}(K/k)| = [K : k]$) and condition (4) ($k = K^{\operatorname{Gal}(K/k)}$). **(1) $\Rightarrow$ (4).** Assume $|G| = [K : k]$ where $G = \operatorname{Gal}(K/k)$. Define the fixed field $F = K^G = \{a \in K : \sigma(a) = a \text{ for all } \sigma \in G\}$. The inclusion $k \subseteq F$ is immediate: every $\sigma \in G$ is a $k$-automorphism, so it fixes $k$ pointwise. Could $F$ be strictly larger than $k$? We show it cannot. Since every element of $G$ fixes $F$, we have $G \leq \operatorname{Aut}_F(K)$, and thus $|G| \leq |\operatorname{Aut}_F(K)|$. By the [Bound on Automorphisms](/theorems/1255) applied to the extension $K/F$, $|\operatorname{Aut}_F(K)| \leq [K : F]$. The chain of inequalities gives \begin{align*} [K : k] = |G| \leq |\operatorname{Aut}_F(K)| \leq [K : F]. \end{align*} But $k \subseteq F \subseteq K$, so by the [Tower Law](/theorems/1248), $[K : k] = [K : F] \cdot [F : k]$. Since $[K : F] \leq [K : k]$ and both are finite, we get $[F : k] = 1$, hence $F = k$. **(4) $\Rightarrow$ (1).** Assume $K^G = k$ where $G = \operatorname{Gal}(K/k)$. Set $n = |G|$. We want to show $[K : k] = n$. The [Bound on Automorphisms](/theorems/1255) gives $n = |G| \leq [K : k]$, so we need the reverse inequality. For any $\alpha \in K$, consider the orbit $G \cdot \alpha = \{\sigma(\alpha) : \sigma \in G\}$ and the polynomial $g_\alpha(x) = \prod_{\beta \in G \cdot \alpha}(x - \beta)$. As argued in the (1) $\Rightarrow$ (2) step, every $\sigma \in G$ permutes $G \cdot \alpha$, so $g_\alpha$ has coefficients in $K^G = k$. Since $g_\alpha(\alpha) = 0$ and $g_\alpha \in k[x]$, the minimal polynomial $m_{\alpha,k}$ divides $g_\alpha$, so \begin{align*} [k(\alpha) : k] = \deg m_{\alpha,k} \leq \deg g_\alpha = |G \cdot \alpha| \leq |G| = n. \end{align*} This bound holds for every $\alpha \in K$. Moreover, $g_\alpha$ has distinct roots (the elements of $G \cdot \alpha$ are distinct), so $m_{\alpha,k}$, being a divisor, also has distinct roots. Hence every element of $K$ is separable over $k$, and $K/k$ is a finite separable extension. The [Primitive Element Theorem](/theorems/1267) now applies: there exists $\gamma \in K$ with $K = k(\gamma)$. Therefore \begin{align*} [K : k] = [k(\gamma) : k] = \deg m_{\gamma,k} \leq n = |G|. \end{align*} Combined with $|G| \leq [K : k]$, we conclude $|G| = [K : k]$.[/guided]