[proofplan] Existence is proved by lifting the minimal polynomial of a primitive element of the residue field extension $\ell/k_K$: a monic lift $f \in \mathcal{O}_K[x]$ of the irreducible $\bar{f} \in k_K[x]$ is itself irreducible, and $L = K[x]/(f)$ has the correct residue field and routine ramification. Uniqueness and the Galois property follow from the [Bijection on Hom-Sets](/theorems/???) for unramified extensions, which provides an isomorphism $\operatorname{Gal}(L/K) \cong \operatorname{Gal}(k_L/k_K)$. [/proofplan] [step:Construct an unramified extension $L/K$ with prescribed residue field $\ell$] Let $\ell/k_K$ be a finite extension of degree $d = [\ell : k_K]$. Since $\ell/k_K$ is a finite extension of finite fields, it is simple: there exists $\bar{\alpha} \in \ell$ with $\ell = k_K(\bar{\alpha})$. Let $\bar{f} \in k_K[x]$ be the minimal polynomial of $\bar{\alpha}$ over $k_K$, so $\bar{f}$ is monic, irreducible in $k_K[x]$, and $\deg \bar{f} = d$. Choose a monic lift $f \in \mathcal{O}_K[x]$ of $\bar{f}$, meaning $f$ is monic of degree $d$ and reduces to $\bar{f}$ modulo $\mathfrak{m}_K$. [claim:$f$ is irreducible over $K$] [/claim] [proof] Suppose $f = g \cdot h$ in $K[x]$ with $1 \leq \deg g, \deg h < d$. By Gauss's lemma for DVRs, we may assume $g, h \in \mathcal{O}_K[x]$ are monic. Reducing modulo $\mathfrak{m}_K$: $\bar{f} = \bar{g} \cdot \bar{h}$ in $k_K[x]$, with $1 \leq \deg \bar{g}, \deg \bar{h} < d$. But $\bar{f}$ is irreducible in $k_K[x]$, a contradiction. So $f$ is irreducible over $K$. [/proof] Set $L = K[x]/(f)$ and let $\alpha \in L$ be the image of $x$. Then $[L : K] = \deg f = d$. [/step] [step:Verify $k_L \cong \ell$ and $e_{L/K} = 1$] The residue field of $L$ contains $k_K$ and the image of $\alpha$ in $k_L$, which satisfies $\bar{f}(\bar{\alpha}) = 0$. So $k_K(\bar{\alpha}) \subseteq k_L$, giving an embedding $\ell \hookrightarrow k_L$. By the fundamental identity $[L:K] = e_{L/K} \cdot f_{L/K}$, we have $d = e_{L/K} \cdot [k_L : k_K]$. Since $\ell \hookrightarrow k_L$, we have $[k_L : k_K] \geq [\ell : k_K] = d$. Combined with $[k_L : k_K] \leq d / e_{L/K} \leq d$, this forces $[k_L : k_K] = d$ and $e_{L/K} = 1$. The embedding $\ell \hookrightarrow k_L$ is therefore an isomorphism: $k_L \cong \ell$ over $k_K$. Since $e_{L/K} = 1$, the extension $L/K$ is unramified with $k_L \cong \ell$. [guided] The key point is the interplay between the degree formula and the embedding of residue fields. We have $d = [L:K] = e_{L/K} f_{L/K}$. The residue field $k_L$ contains a copy of $\ell$ (generated by $\bar{\alpha}$), so $f_{L/K} = [k_L : k_K] \geq [\ell : k_K] = d$. But also $f_{L/K} \leq [L:K]/e_{L/K} \leq d$ since $e_{L/K} \geq 1$. These squeeze $f_{L/K} = d$ and $e_{L/K} = 1$. Why is $e_{L/K} \geq 1$? The ramification index is always a positive integer (it is the index of the value group $|K^\times|$ in $|L^\times|$). [/guided] [/step] [step:Prove uniqueness of the unramified extension via the Hom-set bijection] Let $L'/K$ be another unramified extension with $k_{L'} \cong \ell$ over $k_K$. By the [Bijection on Hom-Sets](/theorems/???), with $M = L'$: \begin{align*} \operatorname{Hom}_{K\text{-Alg}}(L, L') \longleftrightarrow \operatorname{Hom}_{k_K\text{-Alg}}(k_L, k_{L'}). \end{align*} Since $k_L \cong \ell \cong k_{L'}$ over $k_K$, there exists an isomorphism $k_L \xrightarrow{\sim} k_{L'}$ in $\operatorname{Hom}_{k_K\text{-Alg}}(k_L, k_{L'})$. This corresponds to a $K$-algebra homomorphism $\varphi: L \to L'$. Since $[L:K] = [L':K] = d$ and $\varphi$ is injective (as a nonzero field homomorphism), $\varphi$ is an isomorphism. So $L \cong L'$ over $K$. [/step] [step:Establish the Galois property and the isomorphism $\operatorname{Gal}(L/K) \cong \operatorname{Gal}(\ell/k_K)$] Applying the [Bijection on Hom-Sets](/theorems/???) with $M = L$: \begin{align*} \operatorname{Hom}_{K\text{-Alg}}(L, L) \longleftrightarrow \operatorname{Hom}_{k_K\text{-Alg}}(k_L, k_L). \end{align*} The right-hand side is $\operatorname{Aut}_{k_K}(k_L) = \operatorname{Gal}(k_L/k_K)$, since $k_L/k_K$ is a finite extension of finite fields, hence Galois. The left-hand side is $\operatorname{End}_{K\text{-Alg}}(L)$. Since $|\operatorname{Gal}(k_L/k_K)| = [k_L : k_K] = d = [L:K]$, and $|\operatorname{Hom}_{K\text{-Alg}}(L, L)| \leq [L:K]$ (a $K$-algebra endomorphism of $L = K(\alpha)$ is determined by $\varphi(\alpha)$, which must be a root of $f$ in $L$, and $f$ has at most $d$ roots), the bijection gives $|\operatorname{Hom}_{K\text{-Alg}}(L, L)| = d = [L:K]$. Since every $K$-algebra endomorphism of $L$ is injective (as a field homomorphism) and $L$ is finite-dimensional over $K$, every such endomorphism is an automorphism. Therefore $|\operatorname{Aut}_K(L)| = [L:K]$, which means $L/K$ is Galois, and the reduction map induces an isomorphism \begin{align*} \operatorname{Gal}(L/K) \xrightarrow{\;\sim\;} \operatorname{Gal}(k_L/k_K) \cong \operatorname{Gal}(\ell/k_K). \end{align*} [guided] The logic is as follows. An extension $L/K$ of degree $d$ is Galois if and only if $|\operatorname{Aut}_K(L)| = d$. The Hom-set bijection gives $|\operatorname{Hom}_{K\text{-Alg}}(L, L)| = |\operatorname{Gal}(k_L/k_K)| = [k_L:k_K] = d$, using the fact that finite field extensions are always Galois (and cyclic). Every element of $\operatorname{Hom}_{K\text{-Alg}}(L, L)$ is a field endomorphism of a finite extension, hence bijective, hence an automorphism. So $|\operatorname{Aut}_K(L)| = d = [L:K]$, confirming $L/K$ is Galois. The bijection itself provides the isomorphism $\operatorname{Gal}(L/K) \cong \operatorname{Gal}(k_L/k_K)$: each automorphism $\sigma \in \operatorname{Gal}(L/K)$ preserves $\mathcal{O}_L$ and $\mathfrak{m}_L$ (since it is an isometry), hence induces an automorphism $\bar{\sigma}$ of $k_L$ fixing $k_K$. The map $\sigma \mapsto \bar{\sigma}$ is the isomorphism. [/guided] [/step]