[proofplan] We prove each part of the theorem separately. For (i), we show that $k^{\mathrm{sep}}$ is both normal and separable over $k$ by expressing it as a directed union of splitting fields of separable polynomials. For (ii), we use the [Classification of Perfect Fields](/theorems/3324) to relate the Frobenius surjectivity condition to whether every algebraic element is separable. For (iii), we take an arbitrary $\alpha \in \overline{k}$ and show that its minimal polynomial over $k^{\mathrm{sep}}$ has only one distinct root, using the [Decomposition into Separable and Purely Inseparable Parts](/theorems/3332). For (iv), we invoke the [Galois Group as Inverse Limit](/theorems/2362) to realise $G_k$ as an inverse limit of finite groups, and then apply the [Fundamental Theorem of Infinite Galois Theory](/theorems/2387). [/proofplan]

[step:Show that $k^{\mathrm{sep}}/k$ is separable]By definition, $k^{\mathrm{sep}}$ is the set of all elements in $\overline{k}$ that are separable over $k$. Let $\alpha \in k^{\mathrm{sep}}$. Then the minimal polynomial $\operatorname{min}(\alpha, k) \in k[x]$ is separable, so $\alpha$ is separable over $k$. Since every element of $k^{\mathrm{sep}}$ is separable over $k$, the extension $k^{\mathrm{sep}}/k$ is separable. We must verify that $k^{\mathrm{sep}}$ is indeed a field. Let $\alpha, \beta \in k^{\mathrm{sep}}$. The extension $k(\alpha, \beta)/k$ is finite and generated by separable elements. By the [Characterisation of Separable Extensions](/theorems/1265), $k(\alpha, \beta)/k$ is separable, so every element of $k(\alpha, \beta)$ is separable over $k$. In particular, $\alpha + \beta$, $\alpha \beta$, and (when $\alpha \neq 0$) $\alpha^{-1}$ all lie in $k^{\mathrm{sep}}$. Thus $k^{\mathrm{sep}}$ is a subfield of $\overline{k}$.[/step]

[guided]The separable closure $k^{\mathrm{sep}}$ is defined as the set of all elements of $\overline{k}$ that are separable over $k$. We need to verify two things: that $k^{\mathrm{sep}}$ is a field, and that $k^{\mathrm{sep}}/k$ is separable. For the field property, the concern is closure under arithmetic. Take $\alpha, \beta \in k^{\mathrm{sep}}$. Each is separable over $k$, but why should $\alpha + \beta$ be separable over $k$? The key is that $k(\alpha, \beta)/k$ is a finite extension generated by elements whose minimal polynomials over $k$ are separable. The [Characterisation of Separable Extensions](/theorems/1265) tells us that a finite extension generated by elements with separable minimal polynomials is itself separable, meaning every element of $k(\alpha, \beta)$ is separable over $k$. Since $\alpha + \beta, \alpha\beta, \alpha^{-1} \in k(\alpha, \beta)$, they all lie in $k^{\mathrm{sep}}$. That $k^{\mathrm{sep}}/k$ is separable is then immediate from the definition: every element of $k^{\mathrm{sep}}$ has a separable minimal polynomial over $k$.[/guided]

[step:Show that $k^{\mathrm{sep}}/k$ is normal]We must show that $k^{\mathrm{sep}}/k$ is a normal extension, i.e., for every $\alpha \in k^{\mathrm{sep}}$, the minimal polynomial $\operatorname{min}(\alpha, k)$ splits completely in $k^{\mathrm{sep}}[x]$. Let $\alpha \in k^{\mathrm{sep}}$ and let $f = \operatorname{min}(\alpha, k) \in k[x]$. Since $\alpha$ is separable over $k$, the polynomial $f$ is separable. Let $\alpha_1, \ldots, \alpha_n$ be the roots of $f$ in $\overline{k}$. Since $f$ is separable, these roots are distinct, so $\deg f = n$. Each $\alpha_i$ is a root of the same irreducible polynomial $f \in k[x]$, so $\operatorname{min}(\alpha_i, k) = f$, which is separable. Therefore each $\alpha_i \in k^{\mathrm{sep}}$, and $f$ splits completely in $k^{\mathrm{sep}}[x]$. Since $k^{\mathrm{sep}}/k$ is both separable and normal, it is Galois by the [Equivalent Characterisations of Galois Extensions](/theorems/3310) (applied to every finite sub-extension: each finite sub-extension $L/k$ with $L \subset k^{\mathrm{sep}}$ is separable, and the normality of $k^{\mathrm{sep}}/k$ passes to $L/k$ when $L$ is the splitting field of a separable polynomial). More precisely, $k^{\mathrm{sep}} = \bigcup_{\alpha \in k^{\mathrm{sep}}} K_\alpha$, where $K_\alpha$ is the splitting field of $\operatorname{min}(\alpha, k)$ over $k$. Each $K_\alpha/k$ is a finite Galois extension by the [Equivalent Characterisations of Galois Extensions](/theorems/3310), since $K_\alpha$ is the splitting field of a separable polynomial. The union of a directed family of finite Galois extensions is Galois, completing the proof of part (i).[/step]

[guided]We need to show normality: for every $\alpha \in k^{\mathrm{sep}}$, all conjugates of $\alpha$ over $k$ also lie in $k^{\mathrm{sep}}$. Take $\alpha \in k^{\mathrm{sep}}$ and let $f = \operatorname{min}(\alpha, k)$. By definition of $k^{\mathrm{sep}}$, $f$ is separable. Now consider any root $\beta$ of $f$ in $\overline{k}$. Since $\beta$ is also a root of $f$, and $f$ is irreducible over $k$, we have $\operatorname{min}(\beta, k) = f$. The polynomial $f$ is separable, so $\beta$ is separable over $k$, hence $\beta \in k^{\mathrm{sep}}$. This shows that $f$ splits completely in $k^{\mathrm{sep}}[x]$, which is exactly the normality condition. Now, $k^{\mathrm{sep}}/k$ is both normal and separable. For a finite extension, the [Equivalent Characterisations of Galois Extensions](/theorems/3310) would immediately give us that it is Galois. For the possibly infinite extension $k^{\mathrm{sep}}/k$, we argue as follows. For each $\alpha \in k^{\mathrm{sep}}$, the splitting field $K_\alpha$ of $\operatorname{min}(\alpha, k)$ over $k$ is contained in $k^{\mathrm{sep}}$ (since all roots are separable), and $K_\alpha/k$ is a finite Galois extension by the [Equivalent Characterisations of Galois Extensions](/theorems/3310) (it is the splitting field of a separable polynomial). Since $k^{\mathrm{sep}} = \bigcup_\alpha K_\alpha$ and this union is directed (given $K_\alpha, K_\beta$, both are contained in $K_\gamma$ where $\gamma$ is a primitive element of $K_\alpha K_\beta / k$, which exists by the [Primitive Element Theorem](/theorems/1267) since the composite of separable extensions is separable), $k^{\mathrm{sep}}/k$ is a directed union of finite Galois extensions, hence Galois.[/guided]

[step:Prove that $k^{\mathrm{sep}} = \overline{k}$ if and only if $k$ is perfect]($\Rightarrow$) Suppose $k^{\mathrm{sep}} = \overline{k}$. Then every element of $\overline{k}$ is separable over $k$, which means every irreducible polynomial in $k[x]$ is separable. If $\operatorname{char}(k) = 0$, then $k$ is perfect by the [Classification of Perfect Fields](/theorems/3324). If $\operatorname{char}(k) = p > 0$, suppose for contradiction that the Frobenius $\varphi_p: k \to k$, $x \mapsto x^p$, is not surjective. Then there exists $a \in k$ with $a \notin k^p$. The polynomial $x^p - a \in k[x]$ is irreducible (if it factored, say $x^p - a = g(x) h(x)$ with $\deg g = d$, $0 < d < p$, then in $\overline{k}$ we have $x^p - a = (x - \alpha)^p$ where $\alpha^p = a$, so the constant term of $g$ would be $\pm \alpha^d$, giving $\alpha^d \in k$; since $\gcd(d, p) = 1$, Bezout gives integers $r, s$ with $rd + sp = 1$, so $\alpha = \alpha^{rd + sp} = (\alpha^d)^r \cdot (\alpha^p)^s = (\alpha^d)^r a^s \in k$, contradicting $a = \alpha^p \notin k^p$ since $\alpha \in k$ would give $a \in k^p$). But $x^p - a = (x - \alpha)^p$ in $\overline{k}[x]$, so $x^p - a$ has a repeated root and is inseparable. This contradicts the assumption that every irreducible polynomial is separable. Therefore $\varphi_p$ is surjective, and $k$ is perfect by the [Classification of Perfect Fields](/theorems/3324). ($\Leftarrow$) Suppose $k$ is perfect. We show every $\alpha \in \overline{k}$ is separable over $k$. Let $f = \operatorname{min}(\alpha, k)$. By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), if $f$ is inseparable then $\operatorname{char}(k) = p > 0$ and $f(x) = g(x^p)$ for some $g \in k[x]$. Write $g(x) = \sum_{i=0}^m c_i x^i$. Since $k$ is perfect, the Frobenius is surjective, so each $c_i = b_i^p$ for some $b_i \in k$. Then $f(x) = \sum_{i=0}^m b_i^p x^{ip} = \left(\sum_{i=0}^m b_i x^i\right)^p$, contradicting the irreducibility of $f$ (since $\deg f = mp > m$). Therefore $f$ is separable, $\alpha \in k^{\mathrm{sep}}$, and $k^{\mathrm{sep}} = \overline{k}$.[/step]

[guided]We prove both directions of part (ii). **Forward direction.** Assume $k^{\mathrm{sep}} = \overline{k}$, meaning every algebraic element over $k$ is separable. We want to show $k$ is perfect. If $\operatorname{char}(k) = 0$, the [Classification of Perfect Fields](/theorems/3324) immediately gives perfectness. The interesting case is $\operatorname{char}(k) = p > 0$. We need to show the Frobenius $\varphi_p: k \to k$, $x \mapsto x^p$, is surjective. Suppose for contradiction that some $a \in k$ has no $p$-th root in $k$, i.e., $a \notin k^p$. Consider the polynomial $f(x) = x^p - a \in k[x]$. In the algebraic closure, if $\alpha \in \overline{k}$ satisfies $\alpha^p = a$, then $x^p - a = x^p - \alpha^p = (x - \alpha)^p$ (using the Frobenius identity $(x - \alpha)^p = x^p - \alpha^p$ in characteristic $p$). So $f$ has $\alpha$ as a root of multiplicity $p$, making it inseparable. We verify that $f$ is irreducible over $k$. If $f = g \cdot h$ with $1 \le d = \deg g < p$, then since $f = (x - \alpha)^p$ in $\overline{k}[x]$, we have $g(x) = (x - \alpha)^d$. The constant term of $g$ is $(-\alpha)^d \in k$, so $\alpha^d \in k$. Since $d < p$ and $p$ is prime, $\gcd(d, p) = 1$. By Bezout's identity, there exist integers $r, s$ with $rd + sp = 1$. Then $\alpha = \alpha^{rd + sp} = (\alpha^d)^r \cdot (\alpha^p)^s$. We have $\alpha^d \in k$ and $\alpha^p = a \in k$, so $\alpha \in k$, giving $a = \alpha^p \in k^p$, a contradiction. So $f$ is irreducible and inseparable, contradicting $k^{\mathrm{sep}} = \overline{k}$. **Backward direction.** Assume $k$ is perfect. Take any $\alpha \in \overline{k}$ and let $f = \operatorname{min}(\alpha, k)$. We want to show $f$ is separable. By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), if $f$ were inseparable, then $\operatorname{char}(k) = p > 0$ and $f(x) = g(x^p)$ for some $g \in k[x]$. Write $g(x) = \sum_{i=0}^m c_i x^i$. Since $k$ is perfect, the Frobenius is surjective by the [Classification of Perfect Fields](/theorems/3324), so each $c_i = b_i^p$ for some $b_i \in k$. Then: \begin{align*} f(x) = \sum_{i=0}^m b_i^p \, x^{ip} = \left(\sum_{i=0}^m b_i \, x^i\right)^p \end{align*} where the last equality uses the Frobenius identity $(\sum b_i x^i)^p = \sum b_i^p x^{ip}$ in characteristic $p$. This contradicts the irreducibility of $f$, since $\deg g = m < mp = \deg f$. Therefore every irreducible polynomial over $k$ is separable, so every element of $\overline{k}$ is separable over $k$, giving $k^{\mathrm{sep}} = \overline{k}$.[/guided]

[step:Show that $\overline{k} / k^{\mathrm{sep}}$ is purely inseparable]Let $\alpha \in \overline{k}$ and let $f = \operatorname{min}(\alpha, k^{\mathrm{sep}}) \in k^{\mathrm{sep}}[x]$. We must show that $f$ has only one distinct root in $\overline{k}$, i.e., $f(x) = (x - \alpha)^m$ for some $m \ge 1$. If $\operatorname{char}(k) = 0$, then $k$ is perfect, so $k^{\mathrm{sep}} = \overline{k}$ by part (ii), and the statement is vacuous (every element of $\overline{k}$ already lies in $k^{\mathrm{sep}}$). Assume $\operatorname{char}(k) = p > 0$. Consider the finite extension $k(\alpha)/k$. By the [Decomposition into Separable and Purely Inseparable Parts](/theorems/3332), there exists a unique intermediate field $F$ with $k \subset F \subset k(\alpha)$ such that $F/k$ is separable and $k(\alpha)/F$ is purely inseparable. Since $F/k$ is separable, $F \subset k^{\mathrm{sep}}$. Since $k(\alpha)/F$ is purely inseparable, there exists $e \ge 0$ such that $\alpha^{p^e} \in F \subset k^{\mathrm{sep}}$. Set $\beta = \alpha^{p^e} \in k^{\mathrm{sep}}$. The polynomial $x^{p^e} - \beta = (x - \alpha)^{p^e}$ in $\overline{k}[x]$ (using the Frobenius identity in characteristic $p$), and $\alpha$ is a root. The minimal polynomial $\operatorname{min}(\alpha, k^{\mathrm{sep}})$ divides $x^{p^e} - \beta = (x - \alpha)^{p^e}$, so $\operatorname{min}(\alpha, k^{\mathrm{sep}}) = (x - \alpha)^{p^r}$ for some $0 \le r \le e$. This polynomial has $\alpha$ as its only root, so $\alpha$ is purely inseparable over $k^{\mathrm{sep}}$.[/step]

[guided]We want to show that every element of $\overline{k}$ is purely inseparable over $k^{\mathrm{sep}}$. Recall that $\alpha$ is purely inseparable over a field $L$ if and only if $\operatorname{min}(\alpha, L)$ has only one distinct root in $\overline{k}$. If $\operatorname{char}(k) = 0$, then $k$ is perfect, so by part (ii) $k^{\mathrm{sep}} = \overline{k}$, and there is nothing to prove: every element of $\overline{k}$ already lies in $k^{\mathrm{sep}}$ and has minimal polynomial $x - \alpha$. The substantive case is $\operatorname{char}(k) = p > 0$. Take $\alpha \in \overline{k}$. The idea is to use the separable-inseparable decomposition of $k(\alpha)/k$. By the [Decomposition into Separable and Purely Inseparable Parts](/theorems/3332), applied to the finite extension $k(\alpha)/k$, there is a unique intermediate field $F$ with $k \subset F \subset k(\alpha)$ such that $F/k$ is separable and $k(\alpha)/F$ is purely inseparable. Since $F/k$ is separable, every element of $F$ is separable over $k$, so $F \subset k^{\mathrm{sep}}$. Now, $k(\alpha)/F$ is purely inseparable, so there exists $e \ge 0$ with $\alpha^{p^e} \in F$. Set $\beta = \alpha^{p^e}$. Then $\beta \in F \subset k^{\mathrm{sep}}$. Consider the polynomial $x^{p^e} - \beta \in k^{\mathrm{sep}}[x]$. In characteristic $p$, the Frobenius identity gives: \begin{align*} x^{p^e} - \beta = x^{p^e} - \alpha^{p^e} = (x - \alpha)^{p^e}. \end{align*} Since $\alpha$ is a root of $x^{p^e} - \beta$ and this polynomial lies in $k^{\mathrm{sep}}[x]$, the minimal polynomial $\operatorname{min}(\alpha, k^{\mathrm{sep}})$ divides $(x - \alpha)^{p^e}$. Every divisor of $(x - \alpha)^{p^e}$ has $\alpha$ as its only root, so $\operatorname{min}(\alpha, k^{\mathrm{sep}})$ has only one distinct root, confirming that $\alpha$ is purely inseparable over $k^{\mathrm{sep}}$. Note: if $\alpha$ were already in $k^{\mathrm{sep}}$, then $e = 0$, $\beta = \alpha$, and $\operatorname{min}(\alpha, k^{\mathrm{sep}}) = x - \alpha$. The purely inseparable condition is trivially satisfied with inseparable degree $1$.[/guided]

[step:Establish that $G_k$ is profinite via the inverse limit representation]By part (i), $k^{\mathrm{sep}}/k$ is a Galois extension. Let $\mathcal{I}$ denote the directed set of all finite Galois sub-extensions $L/k$ with $L \subset k^{\mathrm{sep}}$, ordered by inclusion. This set is directed: given $L_1, L_2 \in \mathcal{I}$, the composite $L_1 L_2$ is a finite Galois extension of $k$ (as the composite of finite Galois extensions is Galois) contained in $k^{\mathrm{sep}}$, so $L_1 L_2 \in \mathcal{I}$. By the [Galois Group as Inverse Limit](/theorems/2362), the restriction maps $\operatorname{Gal}(L'/k) \to \operatorname{Gal}(L/k)$ for $L \subset L'$ in $\mathcal{I}$ form an inverse system, and \begin{align*} G_k = \operatorname{Gal}(k^{\mathrm{sep}}/k) \cong \varprojlim_{L/k \in \mathcal{I}} \operatorname{Gal}(L/k) \end{align*} as topological groups, where each $\operatorname{Gal}(L/k)$ carries the discrete topology. Each $\operatorname{Gal}(L/k)$ is a finite group (by the [Order of the Galois Group](/theorems/3325), $|\operatorname{Gal}(L/k)| = [L:k] < \infty$). An inverse limit of finite groups with the inverse limit topology is, by definition, a profinite group. By the [Compactness of the Galois Group](/theorems/2386), $G_k$ is compact and Hausdorff in the Krull topology, confirming the profinite structure.[/step]

[guided]A profinite group is, by definition, a compact, Hausdorff, totally disconnected topological group, or equivalently, an inverse limit of finite groups. We show $G_k$ is profinite by realising it as such an inverse limit. Since $k^{\mathrm{sep}}/k$ is Galois (part (i)), every $\alpha \in k^{\mathrm{sep}}$ has a separable minimal polynomial over $k$ that splits in $k^{\mathrm{sep}}$. The splitting field of $\operatorname{min}(\alpha, k)$ is a finite Galois extension of $k$ contained in $k^{\mathrm{sep}}$. Let $\mathcal{I}$ be the collection of all such finite Galois sub-extensions $L/k$. This forms a directed set under inclusion: given $L_1, L_2 \in \mathcal{I}$, the composite $L_1 L_2$ is finite (as both $L_1$ and $L_2$ are finite over $k$), normal (as the composite of normal extensions is normal), and separable (by the [Multiplicativity of Separable Degree](/theorems/3331)), hence Galois by the [Equivalent Characterisations of Galois Extensions](/theorems/3310). The [Galois Group as Inverse Limit](/theorems/2362) applies to the Galois extension $k^{\mathrm{sep}}/k$ with this directed system. For each pair $L \subset L'$ in $\mathcal{I}$, the restriction homomorphism $\operatorname{Gal}(L'/k) \to \operatorname{Gal}(L/k)$, $\sigma \mapsto \sigma|_L$, is well-defined and surjective. The theorem gives: \begin{align*} G_k = \operatorname{Gal}(k^{\mathrm{sep}}/k) \cong \varprojlim_{L/k \in \mathcal{I}} \operatorname{Gal}(L/k) \end{align*} as topological groups. Each $\operatorname{Gal}(L/k)$ is finite by the [Order of the Galois Group](/theorems/3325), with $|\operatorname{Gal}(L/k)| = [L:k]$. An inverse limit of finite discrete groups, equipped with the product topology (restricted to the inverse limit), is compact by Tychonoff and Hausdorff, hence profinite. The [Compactness of the Galois Group](/theorems/2386) confirms that $G_k$ is compact and Hausdorff in the Krull topology.[/guided]

[step:Derive the Galois correspondence for intermediate fields of $k^{\mathrm{sep}}/k$]Since $k^{\mathrm{sep}}/k$ is a Galois extension (part (i)) and $G_k = \operatorname{Gal}(k^{\mathrm{sep}}/k)$ is profinite (as just shown), the [Fundamental Theorem of Infinite Galois Theory](/theorems/2387) applies. It gives a bijection \begin{align*} \{F : k \subset F \subset k^{\mathrm{sep}}\} &\longleftrightarrow \{H \le G_k : H \text{ is closed}\} \\ F &\longmapsto \operatorname{Gal}(k^{\mathrm{sep}}/F) \\ (k^{\mathrm{sep}})^H &\longmapsfrom H. \end{align*} We verify the hypotheses of the [Fundamental Theorem of Infinite Galois Theory](/theorems/2387): $k^{\mathrm{sep}}/k$ is Galois by part (i). The theorem requires no further conditions beyond the extension being Galois. Moreover, an intermediate field $F/k$ is finite if and only if $\operatorname{Gal}(k^{\mathrm{sep}}/F)$ is open in $G_k$, and $F/k$ is Galois if and only if $\operatorname{Gal}(k^{\mathrm{sep}}/F)$ is normal in $G_k$, in which case $\operatorname{Gal}(F/k) \cong G_k / \operatorname{Gal}(k^{\mathrm{sep}}/F)$. This completes the proof of part (iv) and of the theorem.[/step]

[guided]The [Fundamental Theorem of Infinite Galois Theory](/theorems/2387) is the infinite analogue of the [Fundamental Theorem of Galois Theory](/theorems/1274). The finite version gives a bijection between all subgroups of $\operatorname{Gal}(K/k)$ and intermediate fields. For infinite Galois extensions, one must restrict to **closed** subgroups (in the Krull topology) to maintain the bijection. Not every subgroup of the profinite group $G_k$ is closed — for instance, the commutator subgroup of a profinite group may not be closed — and the subgroups that fail to be closed do not correspond to any intermediate field. The theorem applies directly to $k^{\mathrm{sep}}/k$ because this extension is Galois (part (i)). The correspondence is: \begin{align*} F &\longmapsto \operatorname{Gal}(k^{\mathrm{sep}}/F), \\ (k^{\mathrm{sep}})^H &\longmapsfrom H. \end{align*} These maps are mutually inverse: $(k^{\mathrm{sep}})^{\operatorname{Gal}(k^{\mathrm{sep}}/F)} = F$ (which is the content of the Galois correspondence), and $\operatorname{Gal}(k^{\mathrm{sep}} / (k^{\mathrm{sep}})^H) = H$ for $H$ closed (which fails for non-closed $H$, since $\operatorname{Gal}(k^{\mathrm{sep}} / (k^{\mathrm{sep}})^H) = \overline{H}$, the closure of $H$). The additional statements about finiteness and normality are part of the [Fundamental Theorem of Infinite Galois Theory](/theorems/2387): $F/k$ is finite if and only if $\operatorname{Gal}(k^{\mathrm{sep}}/F)$ has finite index in $G_k$, which, in a profinite group, is equivalent to being open. The extension $F/k$ is Galois if and only if $\operatorname{Gal}(k^{\mathrm{sep}}/F)$ is normal, yielding the quotient isomorphism $G_k / \operatorname{Gal}(k^{\mathrm{sep}}/F) \cong \operatorname{Gal}(F/k)$.[/guided]