Solution (source code)

= Solution

Write $\mathcal O$ for the <valuation ring> of $K$, $\pi$ for a <uniformizer>, $v(\pi)=1$, and $k=\mathbb F_q$ for the <residue field>. A useful <strong form of Hensel lemma> is the following: if $f\in\mathcal O[X]$ and $a_0\in\mathcal O$ satisfy
$$
v(f(a_0))>2v(f'(a_0)),
$$
then there is a root $a\in\mathcal O$ with $v(a-a_0)>v(f'(a_0))$, unique among roots in that ball. If $f(a_0)\ne0$, its distance satisfies $v(a-a_0)=v(f(a_0))-v(f'(a_0))$.

Here is a proof by successive correction. Put $s=v(f'(a_0))$, $d_j=v(f(a_j))$, and
$$
a_{j+1}=a_j-\frac{f(a_j)}{f'(a_j)}.
$$
Stop if a root has already been reached. Otherwise the correction has <valuation> $d_j-s>s$. Integral Taylor expansions show that $v(f'(a_{j+1}))=s$ and
$$
d_{j+1}\ge2(d_j-s),\qquad d_{j+1}-2s\ge2(d_j-2s).
$$
Thus $d_j-2s$ grows at least geometrically, the corrections tend to zero, and <completeness> gives a limit $a$ with $f(a)=0$. The first correction has strictly smaller <valuation> than every later nonzero correction, proving the asserted distance. If $x,y$ are in the ball $v(x-a_0),v(y-a_0)>s$, then
$$
f(x)-f(y)=(x-y)\bigl(f'(a_0)+c\bigr),\qquad v(c)>s.
$$
The second factor cannot vanish. Two roots in the ball must therefore coincide. This proves <Hensel lemma>; in particular a simple root modulo $\pi$ has a unique lift with that residue.

We use this to establish <existence and uniqueness of unramified local extensions>. For each integer $d\ge1$, choose a monic <irreducible polynomial> $\bar f\in k[X]$ of degree $d$ and lift it to a monic $f\in\mathcal O[X]$. Reduction and <Gauss lemma> show that $f$ remains irreducible over $K$. Let
$$
A=\mathcal O[X]/(f),\qquad L=K[X]/(f).
$$
The <ring> $A$ is finite free and complete over $\mathcal O$, and $A/\pi A\cong\mathbb F_{q^d}$. An element outside $\pi A$ is invertible: lift an inverse from the <residue field> and invert the remaining $1+\pi z$ by a convergent geometric series. Every nonzero element of $A$ is $\pi^t$ times such a unit, since $\bigcap_t\pi^t A=0$ in a finite free <module>. Thus $A$ is a <discrete valuation ring>, its fraction field is $L$, and
$$
[L:K]=d=[k_L:k],\qquad e(L/K)=1.
$$
This constructs an <unramified extension> of each degree.

Conversely, let $M/K$ be an <unramified extension> of degree $d$. Its <residue field> is the unique degree-$d$ <finite field extension> $\mathbb F_{q^d}/\mathbb F_q$. Choose a residue root of $\bar f$ in it. The root is simple, so <Hensel lemma> lifts it to a root of $f$ in $M$. This embeds $L$ into $M$, and equality of degrees makes it an isomorphism. All $d$ residue conjugates lift in $L$ itself; hence $L/K$ is <Galois>, and reduction identifies its <Galois group> with the cyclic <Galois group> of the <residue field> extension. Its distinguished <Frobenius automorphism> reduces to $x\mapsto x^q$.

\b[There is exactly one unramified extension $K_d$ of each degree inside a fixed algebraic closure], and
$$
\boxed{\operatorname{Gal}(K_d/K)\cong C_d,\qquad K_d=K(\mu_{q^d-1}),\qquad K_a\subseteq K_b\iff a\mid b.}
$$
For the middle equality, every nonzero element of $\mathbb F_{q^d}$ lifts uniquely to a $(q^d-1)$st <root of unity>, because that exponent is prime to $p$. A primitive such residue generates the <finite field extension>, so its lift generates $K_d$. Taking the union gives the <maximal unramified extension>, with <Galois group> $\widehat{\mathbb Z}$.