[proofplan] We prove the equivalences in the cycle (i) $\Rightarrow$ (ii) $\Rightarrow$ (iii) $\Rightarrow$ (iv) $\Rightarrow$ (i). The implication (i) $\Rightarrow$ (ii) uses the primitive element theorem to reduce to a simple extension and checks that $K \otimes_k k^{1/p^\infty}$ has no nilpotents when the minimal polynomial is separable. For (ii) $\Rightarrow$ (iii), we show that if $K \otimes_k k^{1/p^\infty}$ is a field then no inseparable elements exist in $K/k$. The equivalence (i) $\Leftrightarrow$ (iii) is essentially the definition. The implication (iii) $\Rightarrow$ (iv) uses the existence of enough distinct embeddings to make the trace nonzero. The implication (iv) $\Rightarrow$ (i) is proved by contrapositive: if $K/k$ is inseparable, all embeddings coincide on a $p$-th power, forcing the trace to vanish. [/proofplan]

[step:Establish (i) $\Leftrightarrow$ (iii) from the definition]By definition, the separable degree $[K : k]_s$ equals the number of distinct $k$-embeddings $K \hookrightarrow \overline{k}$. The extension $K/k$ is separable if and only if every element of $K$ is separable over $k$. For a finite extension, this is equivalent to $[K : k]_s = [K : k]$: the separable degree equals the full degree precisely when no inseparable factors reduce the embedding count. More concretely, for a simple extension $k(\alpha)/k$ with $\operatorname{min}(\alpha, k)$ of degree $d$, the number of $k$-embeddings $k(\alpha) \hookrightarrow \overline{k}$ equals the number of distinct roots of $\operatorname{min}(\alpha, k)$ in $\overline{k}$. By the [Structure of Simple Algebraic Extensions](/theorems/1251), $[k(\alpha) : k] = d$. So $[k(\alpha) : k]_s = d = [k(\alpha) : k]$ iff $\operatorname{min}(\alpha, k)$ has $d$ distinct roots, i.e., $\alpha$ is separable. For a general finite extension $K = k(\alpha_1, \ldots, \alpha_r)$, the [Multiplicativity of Separable Degree](/theorems/3331) and induction on the tower give the equivalence.[/step]

[guided]The equivalence (i) $\Leftrightarrow$ (iii) is the fundamental characterisation of separable extensions in terms of embeddings. Let us verify it carefully. For a simple extension $k(\alpha)/k$: the $k$-embeddings $\sigma: k(\alpha) \hookrightarrow \overline{k}$ correspond bijectively to the roots of $\operatorname{min}(\alpha, k)$ in $\overline{k}$, via $\sigma \mapsto \sigma(\alpha)$. This is because $\sigma$ is determined by $\sigma(\alpha)$ (by the [Structure of Simple Algebraic Extensions](/theorems/1251), every element of $k(\alpha)$ is a polynomial in $\alpha$), and $\sigma(\alpha)$ must be a root of $\operatorname{min}(\alpha, k)$ (applying $\sigma$ to $\operatorname{min}(\alpha, k)(\alpha) = 0$ gives $\operatorname{min}(\alpha, k)(\sigma(\alpha)) = 0$ since $\sigma|_k = \operatorname{id}$). Conversely, every root $\beta$ of $\operatorname{min}(\alpha, k)$ defines an embedding via the isomorphism $k(\alpha) \cong k[x]/(\operatorname{min}(\alpha, k))$ and the evaluation $x \mapsto \beta$. So $[k(\alpha) : k]_s$ = number of distinct roots of $\operatorname{min}(\alpha, k)$, and $[k(\alpha) : k] = \deg \operatorname{min}(\alpha, k)$. These are equal iff $\operatorname{min}(\alpha, k)$ has no repeated roots, i.e., $\alpha$ is separable. For a general finite extension $K/k$: write $K = k(\alpha_1, \ldots, \alpha_r)$ and build the tower $k \subset k(\alpha_1) \subset k(\alpha_1, \alpha_2) \subset \cdots \subset K$. By the [Multiplicativity of Separable Degree](/theorems/3331), $[K : k]_s = \prod [k(\alpha_1, \ldots, \alpha_i) : k(\alpha_1, \ldots, \alpha_{i-1})]_s$ and similarly for degrees. Each factor satisfies $[\cdot]_s \leq [\cdot]$, with equality iff the added element is separable. So the product equals $[K : k]$ iff each $\alpha_i$ is separable over $k(\alpha_1, \ldots, \alpha_{i-1})$, which by the [Multiplicativity of Separable Degree](/theorems/3331) is equivalent to $K/k$ being separable.[/guided]

[step:Prove (i) $\Rightarrow$ (ii): separability implies $K \otimes_k k^{1/p^\infty}$ is a field]Assume $K/k$ is separable and finite. By the [Primitive Element Theorem](/theorems/1267), $K = k(\alpha)$ for some $\alpha \in K$ with separable minimal polynomial $f = \operatorname{min}(\alpha, k) \in k[x]$ of degree $n = [K : k]$. By the [Structure of Simple Algebraic Extensions](/theorems/1251), $K \cong k[x]/(f)$. Therefore \begin{align*} K \otimes_k k^{1/p^\infty} \cong k^{1/p^\infty}[x]/(f), \end{align*} where we view $f$ as a polynomial in $k^{1/p^\infty}[x]$ (since $k \subset k^{1/p^\infty}$). We show $f$ remains irreducible over $k^{1/p^\infty}$. Suppose $f = g \cdot h$ in $k^{1/p^\infty}[x]$ with $\deg g, \deg h \geq 1$. Since $k^{1/p^\infty}$ is a purely inseparable extension of $k$, every $k$-automorphism $\tau$ of $\overline{k}$ fixes $k^{1/p^\infty}$ pointwise (an element $c \in k^{1/p^e}$ satisfies $c^{p^e} \in k$, so $\tau(c)^{p^e} = \tau(c^{p^e}) = c^{p^e}$, and since $x \mapsto x^{p^e}$ is injective in characteristic $p$, $\tau(c) = c$). Therefore $\tau(g) = g$ and $\tau(h) = h$, so the roots $S$ of $g$ in $\overline{k}$ form a subset of the roots of $f$ that is stable under $\operatorname{Gal}(\overline{k}/k)$. Since $f$ is irreducible over $k$, the Galois group acts transitively on the roots of $f$. A nonempty Galois-stable subset of a transitive action must be the entire set, so $S$ is all roots of $f$, contradicting $\deg g < \deg f$. Therefore $f$ is irreducible over $k^{1/p^\infty}$, and $K \otimes_k k^{1/p^\infty} \cong k^{1/p^\infty}[x]/(f)$ is a field.[/step]

[guided]The [Primitive Element Theorem](/theorems/1267) applies since $K/k$ is finite and separable, giving $K = k(\alpha)$. The condition for the Primitive Element Theorem is exactly that the extension be finite and separable, both of which hold. We have $K \cong k[x]/(f)$ where $f = \operatorname{min}(\alpha, k)$ by the [Structure of Simple Algebraic Extensions](/theorems/1251). Base change gives \begin{align*} K \otimes_k k^{1/p^\infty} \cong k^{1/p^\infty}[x]/(f). \end{align*} This is a field if and only if $f$ is irreducible in $k^{1/p^\infty}[x]$. So we need to show that the irreducible separable polynomial $f \in k[x]$ stays irreducible over $k^{1/p^\infty}$. Why should $f$ remain irreducible? The key is that $f$ is separable. Suppose $f = g \cdot h$ in $k^{1/p^\infty}[x]$ with $\deg g, \deg h \geq 1$. In $\overline{k}$, the roots of $g$ form a nonempty proper subset $S$ of the roots of $f$. The roots of $f$ are exactly the conjugates $\{\sigma(\alpha) : \sigma \in \operatorname{Emb}_k(K, \overline{k})\}$. The monic polynomial $\prod_{\beta \in S}(x - \beta)$ has coefficients that are elementary symmetric functions of elements of $S$. We claim these coefficients lie in $k$. The key observation is that $k^{1/p^\infty}$ is a purely inseparable extension of $k$, so every $k$-automorphism of $\overline{k}$ fixes $k^{1/p^\infty}$ pointwise. To verify this: if $c \in k^{1/p^e}$, then $c^{p^e} \in k$, so for any $\tau \in \operatorname{Gal}(\overline{k}/k)$, $\tau(c)^{p^e} = \tau(c^{p^e}) = c^{p^e}$. Since the map $x \mapsto x^{p^e}$ is injective in characteristic $p$, $\tau(c) = c$. Since $\tau$ fixes the coefficients of $g$ and $h$, we have $\tau(g) = g$ and $\tau(h) = h$. Therefore $\tau$ permutes the roots of $g$ among themselves — the root set $S$ of $g$ is stable under $\operatorname{Gal}(\overline{k}/k)$. Now we use that $f$ is irreducible over $k$: the Galois group $\operatorname{Gal}(\overline{k}/k)$ acts transitively on the roots of $f$. A nonempty Galois-stable subset of a transitive action must be the entire set. So $S$ equals the full root set of $f$, contradicting $\deg g < \deg f$. Therefore $f$ is irreducible over $k^{1/p^\infty}$, and $K \otimes_k k^{1/p^\infty}$ is a field.[/guided]

[step:Prove (ii) $\Rightarrow$ (i): $K \otimes_k k^{1/p^\infty}$ being a field implies separability]Assume $K \otimes_k k^{1/p^\infty}$ is a field (equivalently, $K$ and $k^{1/p^\infty}$ are linearly disjoint over $k$). Suppose for contradiction that $K/k$ is not separable. Then there exists $\alpha \in K$ whose minimal polynomial $f = \operatorname{min}(\alpha, k) \in k[x]$ is inseparable. By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), $f(x) = g(x^p)$ for some $g \in k[x]$. Write $f(x) = \sum_{j=0}^{m} a_j x^{jp}$ with $a_m \ne 0$. In $k^{1/p^\infty}$, every element of $k$ has a $p$-th root, so define $b_j = a_j^{1/p} \in k^{1/p} \subset k^{1/p^\infty}$. Then \begin{align*} f(x) = \sum_{j=0}^{m} b_j^p x^{jp} = \left(\sum_{j=0}^{m} b_j x^j\right)^p =: q(x)^p \end{align*} in $k^{1/p^\infty}[x]$, using the Frobenius identity $(a + b)^p = a^p + b^p$ in characteristic $p$. Now consider $K \otimes_k k^{1/p^\infty} \cong k^{1/p^\infty}[x]/(f) = k^{1/p^\infty}[x]/(q^p)$. The element $\bar{q} = q + (q^p) \in k^{1/p^\infty}[x]/(q^p)$ satisfies $\bar{q}^p = q^p + (q^p) = 0$, yet $\bar{q} \ne 0$ (since $\deg q = m < mp = \deg f$, so $q \notin (q^p)$). Therefore $\bar{q}$ is a nonzero nilpotent element, and $k^{1/p^\infty}[x]/(q^p)$ is not a field (a field has no nonzero nilpotents). This contradicts the assumption.[/step]

[guided]We prove the contrapositive: if $K/k$ is not separable, then $K \otimes_k k^{1/p^\infty}$ is not a field. If $K/k$ is inseparable, there exists $\alpha \in K$ with inseparable minimal polynomial $f = \operatorname{min}(\alpha, k)$. By the [Criterion for Inseparability of Irreducible Polynomials](/theorems/3330), $f(x) = g(x^p)$ for some $g \in k[x]$, i.e., $f$ involves only $p$-th powers of $x$: \begin{align*} f(x) = a_0 + a_1 x^p + a_2 x^{2p} + \cdots + a_m x^{mp}. \end{align*} The field $k^{1/p^\infty}$ contains $p$-th roots (and all $p^e$-th roots) of every element of $k$. Let $b_j = a_j^{1/p} \in k^{1/p}$. Using the Frobenius identity in characteristic $p$ — which says $(c + d)^p = c^p + d^p$ for all elements — we get \begin{align*} f(x) = \sum_{j=0}^m b_j^p x^{jp} = \left(\sum_{j=0}^m b_j x^j\right)^p = q(x)^p, \end{align*} where $q(x) = \sum_{j=0}^m b_j x^j \in k^{1/p}[x] \subset k^{1/p^\infty}[x]$. So over $k^{1/p^\infty}$, the irreducible $f$ becomes a perfect $p$-th power. Now the base change gives $K \otimes_k k^{1/p^\infty} \cong k^{1/p^\infty}[x]/(f) = k^{1/p^\infty}[x]/(q^p)$. Consider the image of $q$ in this quotient ring: $\bar{q} = q \bmod (q^p)$. We have $\bar{q}^p = \overline{q^p} = 0$, so $\bar{q}$ is nilpotent. But $\bar{q} \ne 0$: since $\deg q = m$ and $\deg q^p = mp = \deg f$, the polynomial $q$ has degree strictly less than $\deg f$, so $q$ is not a multiple of $q^p = f$ in $k^{1/p^\infty}[x]$, meaning $q \notin (f)$. A field has no nonzero nilpotent elements (if $a^p = 0$ in a field, then $a = 0$). Since $\bar{q}$ is a nonzero nilpotent, $K \otimes_k k^{1/p^\infty}$ is not a field.[/guided]

[step:Prove (i) $\Rightarrow$ (iv): separability implies the trace is nonzero]Assume $K/k$ is separable with $[K : k] = n$. Then $[K : k]_s = n$, so there are exactly $n$ distinct $k$-embeddings $\sigma_1, \ldots, \sigma_n: K \hookrightarrow \overline{k}$. By the [Primitive Element Theorem](/theorems/1267), $K = k(\alpha)$ for some $\alpha$ with $\operatorname{min}(\alpha, k)$ of degree $n$. The roots $\alpha_1 = \sigma_1(\alpha), \ldots, \alpha_n = \sigma_n(\alpha)$ are all distinct (since $\operatorname{min}(\alpha, k)$ is separable of degree $n$). The trace is \begin{align*} \operatorname{Tr}_{K/k}(\alpha) = \sum_{i=1}^{n} \sigma_i(\alpha) = \sum_{i=1}^{n} \alpha_i. \end{align*} By the [Trace and Norm via Minimal Polynomial](/theorems/1292), with $\operatorname{min}(\alpha, k) = x^n + a_{n-1}x^{n-1} + \cdots + a_0$ and $r = [K : k(\alpha)] = 1$, we have $\operatorname{Tr}_{K/k}(\alpha) = -a_{n-1}$. To show the trace map is not identically zero, we use the Dedekind independence of characters. The embeddings $\sigma_1, \ldots, \sigma_n: K \to \overline{k}$ are distinct field homomorphisms, hence linearly independent over $\overline{k}$ by Dedekind's lemma on the independence of characters. Therefore the $k$-linear map $\operatorname{Tr}_{K/k} = \sum_{i=1}^n \sigma_i$ is a nonzero $k$-linear functional (it is a nontrivial $\overline{k}$-linear combination of linearly independent maps, hence nonzero as a function).[/step]

[guided]Assume $K/k$ is separable. The trace $\operatorname{Tr}_{K/k}: K \to k$ is defined by $\operatorname{Tr}_{K/k}(\alpha) = \sum_{\sigma} \sigma(\alpha)$, summing over all $n = [K : k]$ distinct $k$-embeddings $\sigma: K \hookrightarrow \overline{k}$. To show $\operatorname{Tr}_{K/k} \ne 0$, we invoke Dedekind's lemma on the independence of characters: distinct field homomorphisms $\sigma_1, \ldots, \sigma_n: K \to \overline{k}$ are linearly independent over $\overline{k}$. This means: if $c_1, \ldots, c_n \in \overline{k}$ satisfy $\sum_{i=1}^n c_i \sigma_i(\alpha) = 0$ for all $\alpha \in K$, then $c_1 = \cdots = c_n = 0$. Taking $c_1 = \cdots = c_n = 1 \in \overline{k}$: the map $\alpha \mapsto \sum_{i=1}^n 1 \cdot \sigma_i(\alpha) = \operatorname{Tr}_{K/k}(\alpha)$ is a nontrivial linear combination (since $n \geq 1$ and the coefficients are all $1 \ne 0$). By Dedekind's lemma, this map is not identically zero. Hence $\operatorname{Tr}_{K/k} \ne 0$.[/guided]

[step:Prove (iv) $\Rightarrow$ (i): nonvanishing trace implies separability]We prove the contrapositive: if $K/k$ is not separable, then $\operatorname{Tr}_{K/k} \equiv 0$. Assume $K/k$ is inseparable. By the [Decomposition into Separable and Purely Inseparable Parts](/theorems/3332), there is a unique intermediate field $F$ with $F/k$ separable and $K/F$ purely inseparable. Since $K/k$ is inseparable, $K \ne F$, so $[K : F] = p^e$ for some $e \geq 1$. For any $\alpha \in K$, $\alpha^{p^e} \in F$ (since $K/F$ is purely inseparable). The minimal polynomial of $\alpha$ over $F$ divides $x^{p^e} - \alpha^{p^e} = (x - \alpha)^{p^e}$ in $\overline{k}[x]$, so it equals $(x - \alpha)^{p^f}$ for some $1 \leq f \leq e$ (with $p^f = [F(\alpha) : F]$). In particular, $\alpha$ is the unique root of $\operatorname{min}(\alpha, F)$. Now consider the $k$-embeddings $\sigma: K \hookrightarrow \overline{k}$. There are $[K : k]_s$ of them. Each $\sigma$ restricts to a $k$-embedding of $F$, and there are $[F : k]_s = [F : k]$ such embeddings (since $F/k$ is separable). For each $k$-embedding $\tau: F \hookrightarrow \overline{k}$, the extensions $\sigma: K \hookrightarrow \overline{k}$ with $\sigma|_F = \tau$ correspond to roots of $\tau(\operatorname{min}(\alpha, F))$ in $\overline{k}$... More directly: since $K/F$ is purely inseparable, $[K : F]_s = 1$. By the [Multiplicativity of Separable Degree](/theorems/3331), $[K : k]_s = [K : F]_s \cdot [F : k]_s = 1 \cdot [F : k] = [F : k]$. So the $k$-embeddings $K \hookrightarrow \overline{k}$ are in bijection with the $k$-embeddings $F \hookrightarrow \overline{k}$: each embedding of $F$ extends uniquely to $K$ (because the minimal polynomial of any element of $K$ over $F$ has a unique root in $\overline{k}$). Let $\sigma_1, \ldots, \sigma_m$ be the $m = [F : k]$ distinct $k$-embeddings $K \hookrightarrow \overline{k}$. For any $\alpha \in K$, since $\alpha^{p^e} \in F$ and $\sigma_i|_F$ ranges over all $k$-embeddings of $F$, and since $\alpha$ is the unique root of its minimal polynomial over $F$: \begin{align*} \sigma_i(\alpha)^{p^e} = \sigma_i(\alpha^{p^e}) \quad \text{for all } i. \end{align*} But the trace is defined as the sum over all $[K : k]$ embeddings counted with multiplicity. More precisely, the trace $\operatorname{Tr}_{K/k}(\alpha) = \sum_{\sigma} \sigma(\alpha)$ where the sum is over all $[K : k]_s = [F : k]$ embeddings, each counted with multiplicity $[K : k] / [K : k]_s = p^e$: \begin{align*} \operatorname{Tr}_{K/k}(\alpha) = \frac{[K:k]}{[K:k]_s} \sum_{i=1}^{m} \sigma_i(\alpha) = p^e \sum_{i=1}^{m} \sigma_i(\alpha). \end{align*} Since $\operatorname{char}(k) = p$ and $e \geq 1$, the factor $p^e = 0$ in $k$. Therefore $\operatorname{Tr}_{K/k}(\alpha) = 0$ for all $\alpha \in K$.[/step]

[guided]We prove: $K/k$ inseparable implies $\operatorname{Tr}_{K/k} \equiv 0$. By the [Decomposition into Separable and Purely Inseparable Parts](/theorems/3332), $K/k$ decomposes as $k \subset F \subset K$ with $F/k$ separable and $K/F$ purely inseparable. Since $K/k$ is inseparable, $F \ne K$, so $[K : F] = p^e$ with $e \geq 1$. Since $K/F$ is purely inseparable, $[K : F]_s = 1$: for every $\alpha \in K$, the minimal polynomial of $\alpha$ over $F$ has the form $(x - \alpha)^{p^f}$ in $\overline{k}[x]$, so $\alpha$ is the only root, meaning each $F$-embedding extends uniquely. By the [Multiplicativity of Separable Degree](/theorems/3331): \begin{align*} [K : k]_s = [K : F]_s \cdot [F : k]_s = 1 \cdot [F : k] = [F : k] = \frac{[K : k]}{p^e}. \end{align*} The trace map $\operatorname{Tr}_{K/k}$ is defined as $\operatorname{Tr}_{K/k}(\alpha) = \sum_{\sigma} \sigma(\alpha)$, where the sum runs over $k$-embeddings $\sigma: K \hookrightarrow \overline{k}$, with each of the $[K : k]_s$ distinct embeddings counted with multiplicity $[K : k]/[K : k]_s = p^e$. (This multiplicity arises from the inseparable part: the minimal polynomial of an element over an intermediate field has a root of multiplicity $p^f$, and these multiplicities aggregate to give an overall multiplicity of $p^e$.) Therefore: \begin{align*} \operatorname{Tr}_{K/k}(\alpha) = p^e \cdot \sum_{i=1}^{[F:k]} \sigma_i(\alpha), \end{align*} where $\sigma_1, \ldots, \sigma_{[F:k]}$ are the distinct $k$-embeddings of $K$ into $\overline{k}$. Since $p^e \cdot 1_k = 0$ in a field of characteristic $p$ (as $e \geq 1$), the entire expression vanishes: $\operatorname{Tr}_{K/k}(\alpha) = 0$ for every $\alpha \in K$. This completes the proof that inseparability forces the trace to vanish, establishing (iv) $\Rightarrow$ (i) by contrapositive.[/guided]

[step:Conclude the equivalence of all four conditions] Combining the results: - (i) $\Leftrightarrow$ (iii): established in the first step. - (i) $\Rightarrow$ (ii): shown by the primitive element theorem and irreducibility of the minimal polynomial over $k^{1/p^\infty}$. - (ii) $\Rightarrow$ (i): shown by contrapositive — inseparability produces a nilpotent in $K \otimes_k k^{1/p^\infty}$. - (i) $\Rightarrow$ (iv): Dedekind independence of characters. - (iv) $\Rightarrow$ (i): contrapositive — inseparability forces $\operatorname{Tr}_{K/k} = p^e \cdot (\cdots) = 0$. Therefore (i), (ii), (iii), and (iv) are all equivalent. [/step]