[proofplan] We show that the maximal unramified extension $M/K$ is Galois and that reduction modulo the maximal ideal induces an isomorphism $\operatorname{Gal}(M/K) \cong \operatorname{Gal}(k_M/k_K)$ of topological groups. The argument proceeds by passing to inverse limits: every finite subextension $L/K$ of $M/K$ is unramified and hence Galois with $\operatorname{Gal}(L/K) \cong \operatorname{Gal}(k_L/k_K)$ via the reduction map. We then assemble these finite isomorphisms into an isomorphism of inverse limits, using the [Galois Group as Inverse Limit](/theorems/???) to identify both sides. [/proofplan] [step:Show $M/K$ is Galois by verifying normality and separability] Let $M = K^{\mathrm{ur}}$ denote the maximal unramified extension of $K$. Every element $\alpha \in M$ lies in some finite subextension $L/K$ of $M/K$. By definition of $M$, every finite subextension $L/K$ is unramified, and a finite unramified extension of a local field is separable (the residue field extension $k_L/k_K$ is separable, and the minimal polynomial of a uniformiser lift is an Eisenstein polynomial, but more directly: unramified extensions are generated by roots of separable polynomials lifting from the residue field). **Separability.** Every $\alpha \in M$ is separable over $K$: choose a finite subextension $L/K$ containing $\alpha$. Since $L/K$ is unramified, $L/K$ is separable, so $\alpha$ is separable over $K$. **Normality.** Let $\alpha \in M$ and let $f = \operatorname{min}_K(\alpha)$ be its minimal polynomial over $K$. We must show that $f$ splits completely in $M$. Let $L/K$ be a finite unramified extension with $\alpha \in L$, and let $L'$ be the splitting field of $f$ over $K$. Since $L/K$ is unramified and Galois (as the splitting field of a separable polynomial whose roots lie in $L$), and since any conjugate of $\alpha$ over $K$ generates an extension of the same residue degree, the splitting field $L'$ is also an unramified extension of $K$. Therefore $L' \subseteq M$, and $f$ splits completely in $M$. Since $M/K$ is both separable and normal, $M/K$ is Galois. [/step] [step:Recall the finite-level isomorphism $\operatorname{Gal}(L/K) \cong \operatorname{Gal}(k_L/k_K)$ for finite unramified extensions] For each finite unramified extension $L/K$, the reduction map \begin{align*} \operatorname{red}_{L/K} \colon \operatorname{Gal}(L/K) &\to \operatorname{Gal}(k_L/k_K) \\ \sigma &\mapsto \bar{\sigma} \end{align*} is defined by $\bar{\sigma}(\bar{x}) = \overline{\sigma(x)}$ for $x \in \mathcal{O}_L$, where $\bar{x} = x + \mathfrak{m}_L$ denotes the reduction modulo the maximal ideal $\mathfrak{m}_L$ of $\mathcal{O}_L$. This map is well-defined because $\sigma(\mathfrak{m}_L) = \mathfrak{m}_L$ (since $\sigma$ preserves the valuation on $L$ and hence preserves the maximal ideal). Since $L/K$ is unramified, the inertia group $I(L/K) = \ker(\operatorname{red}_{L/K})$ is trivial: $e_{L/K} = 1$ implies $|I(L/K)| = e_{L/K} = 1$. Therefore $\operatorname{red}_{L/K}$ is injective. Comparing orders: $|\operatorname{Gal}(L/K)| = [L : K] = f_{L/K} = [k_L : k_K] = |\operatorname{Gal}(k_L/k_K)|$ (where $f_{L/K}$ is the residue degree and the last equality holds because $k_L/k_K$ is a finite extension of finite fields, hence cyclic Galois). An injective map between finite sets of equal cardinality is a bijection, so $\operatorname{red}_{L/K}$ is an isomorphism. [/step] [step:Assemble the finite isomorphisms into an isomorphism of inverse limits] Let $I$ denote the directed set of finite unramified subextensions $L/K$ of $M/K$, ordered by inclusion. For $L \subseteq L'$ in $I$, the diagram \begin{align*} \operatorname{Gal}(L'/K) &\xrightarrow{\operatorname{red}_{L'/K}} \operatorname{Gal}(k_{L'}/k_K) \\ \downarrow^{\operatorname{res}_{L'/L}} & \qquad \downarrow^{\operatorname{res}_{k_{L'}/k_L}} \\ \operatorname{Gal}(L/K) &\xrightarrow{\operatorname{red}_{L/K}} \operatorname{Gal}(k_L/k_K) \end{align*} commutes: for $\sigma \in \operatorname{Gal}(L'/K)$ and $x \in \mathcal{O}_L$, we have $\operatorname{red}_{L/K}(\sigma|_L)(\bar{x}) = \overline{\sigma|_L(x)} = \overline{\sigma(x)} = \operatorname{red}_{L'/K}(\sigma)|_{k_L}(\bar{x})$. Since each $\operatorname{red}_{L/K}$ is an isomorphism and the diagrams commute, the universal property of inverse limits gives an isomorphism \begin{align*} \varprojlim_{L/K \in I} \operatorname{Gal}(L/K) \xrightarrow{\;\sim\;} \varprojlim_{L/K \in I} \operatorname{Gal}(k_L/k_K). \end{align*} By the [Galois Group as Inverse Limit](/theorems/???), the left-hand side is isomorphic to $\operatorname{Gal}(M/K)$ via $\sigma \mapsto (\sigma|_L)_{L \in I}$. [guided] The inverse limit on the right-hand side deserves identification. We claim it equals $\operatorname{Gal}(k_M/k_K)$. The residue field of $M = K^{\mathrm{ur}}$ is $k_M = \bigcup_{L \in I} k_L$. Since each $k_L/k_K$ is a finite extension of the finite field $k_K$, and every finite extension of $k_K$ arises as the residue field of some unramified extension of $K$, we have $k_M = \overline{k_K}$, the algebraic closure of $k_K$. The extension $k_M/k_K$ is Galois (as a union of finite Galois extensions), and by the [Galois Group as Inverse Limit](/theorems/???) applied to $k_M/k_K$: \begin{align*} \operatorname{Gal}(k_M/k_K) \cong \varprojlim_{k_L/k_K} \operatorname{Gal}(k_L/k_K). \end{align*} The directed systems $\{L/K : L/K \text{ finite unramified}\}$ and $\{k_L/k_K : L/K \text{ finite unramified}\}$ are in bijection (via $L \mapsto k_L$), so the two inverse limits on the right are taken over the same index set. The identification $\varprojlim \operatorname{Gal}(k_L/k_K) \cong \operatorname{Gal}(k_M/k_K)$ is then immediate. [/guided] [/step] [step:Conclude the topological isomorphism $\operatorname{Gal}(M/K) \cong \operatorname{Gal}(k_M/k_K)$] Combining the identifications from the previous steps: \begin{align*} \operatorname{Gal}(M/K) \cong \varprojlim_{L/K \in I} \operatorname{Gal}(L/K) \xrightarrow{\;\sim\;} \varprojlim_{L/K \in I} \operatorname{Gal}(k_L/k_K) \cong \operatorname{Gal}(k_M/k_K). \end{align*} The first isomorphism is the [Galois Group as Inverse Limit](/theorems/???). The middle isomorphism is induced by the compatible family of reduction maps $(\operatorname{red}_{L/K})_{L \in I}$. The last isomorphism is again the [Galois Group as Inverse Limit](/theorems/???) applied to the residue field extension $k_M/k_K$. All three maps are continuous group homomorphisms between profinite groups (inverse limits of finite discrete groups carry the profinite topology, and all maps are defined via compatible families of continuous maps between discrete groups). A continuous bijective group homomorphism between compact Hausdorff topological groups is automatically a homeomorphism (the image of a closed set under a continuous bijection from a compact space to a Hausdorff space is closed, so the map is closed, hence open). Therefore the composite is an isomorphism of topological groups. [/step]