[proofplan] We prove $K^{\mathrm{ab}} = K^{\mathrm{ur}} L_\infty$ by showing that every finite abelian extension $M/K$ is contained in $K_m L_n$ for some $m, n$, where $K_m$ is the unramified extension of degree $m$ and $L_n = K(F(n))$ is the $n$-th Lubin--Tate extension. The proof uses the [Local Artin Reciprocity](/theorems/???) map and the [Existence Theorem](/theorems/???). The reciprocity map identifies $K^\times / N_{M/K}(M^\times)$ with $\operatorname{Gal}(M/K)$ for any finite abelian $M/K$. The norm group $N_{M/K}(M^\times)$ is an open subgroup of finite index in $K^\times$. The key computation is that the norm group of $K_m L_n$ is $\langle \pi^m \rangle \cdot U_K^{(n)}$, and every open subgroup of finite index in $K^\times$ contains such a subgroup. [/proofplan] [step:Compute the norm group of $K_m L_n / K$] The extension $K_m L_n / K$ is the compositum of the unramified extension $K_m / K$ (of degree $m$) and the totally ramified Lubin--Tate extension $L_n / K$. By the [Local Artin Reciprocity](/theorems/???), the norm group $N(K_m L_n / K) = N_{K_m L_n / K}((K_m L_n)^\times)$ corresponds to $\operatorname{Gal}(K_m L_n / K)$ via the Artin map. The norm group of the unramified extension $K_m / K$ is $\langle \pi \rangle \cdot U_K = \pi^{m\mathbb{Z}} \cdot U_K$ — more precisely, $N(K_m / K) = \{a \in K^\times : v_K(a) \in m\mathbb{Z}\} \cdot U_K$... We use instead the standard computation: $\operatorname{Art}_K(\pi)$ restricts to the Frobenius on $K^{\mathrm{ur}}$, and $\operatorname{Art}_K(U_K)$ acts directly on $K^{\mathrm{ur}}$. Therefore $\operatorname{Art}_K^{-1}(\operatorname{Gal}(K^{\mathrm{ab}} / K_m)) = \{\pi^{mk} u : k \in \mathbb{Z}, u \in U_K\} = \langle \pi^m \rangle \cdot U_K$. For the Lubin--Tate extension $L_n / K$: by the [Automorphisms of Division Points](/theorems/???), $\operatorname{Gal}(L_n / K) \cong U_K / U_K^{(n)}$, and the Artin map sends $U_K$ onto $\operatorname{Gal}(L_n / K)$ with kernel $U_K^{(n)}$. Also, $\operatorname{Art}_K(\pi)$ acts directly on $L_n$ (since $\pi$ is the uniformizer used to construct the Lubin--Tate module, and $[\pi]_F$ kills $F(n)$). Therefore $\operatorname{Art}_K^{-1}(\operatorname{Gal}(K^{\mathrm{ab}} / L_n)) = \langle \pi \rangle \cdot U_K^{(n)}$. For the compositum $K_m L_n$: $\operatorname{Gal}(K^{\mathrm{ab}} / K_m L_n) = \operatorname{Gal}(K^{\mathrm{ab}} / K_m) \cap \operatorname{Gal}(K^{\mathrm{ab}} / L_n)$, so \begin{align*} N(K_m L_n / K) = \operatorname{Art}_K^{-1}(\operatorname{Gal}(K^{\mathrm{ab}} / K_m L_n)) = \langle \pi^m \rangle \cdot U_K \;\cap\; \langle \pi \rangle \cdot U_K^{(n)} = \langle \pi^m \rangle \cdot U_K^{(n)}. \end{align*} The last equality holds because an element $\pi^a u$ (with $u \in U_K$) lies in both subgroups if and only if $m \mid a$ and $u \in U_K^{(n)}$. [guided] This step computes the norm group of the compositum $K_m L_n$ by intersecting the norm groups of $K_m$ and $L_n$. The key facts are: 1. **Unramified norm group.** The Artin map $\operatorname{Art}_K \colon K^\times \to \operatorname{Gal}(K^{\mathrm{ab}}/K)$ sends the uniformizer $\pi$ to the arithmetic Frobenius on $K^{\mathrm{ur}}$. The Frobenius generates $\operatorname{Gal}(K_m/K) \cong \mathbb{Z}/m\mathbb{Z}$, so $\operatorname{Art}_K(\pi)$ has order $m$ when restricted to $K_m$. Units $u \in U_K$ act directly on $K^{\mathrm{ur}}$ (they lie in the inertia component). So the kernel of $\operatorname{Art}_K|_{K_m}$ is $\langle \pi^m \rangle \cdot U_K$. 2. **Lubin--Tate norm group.** The Artin map sends $U_K$ onto $\operatorname{Gal}(L_n/K) \cong U_K/U_K^{(n)}$ with kernel $U_K^{(n)}$. The uniformizer $\pi$ acts directly on $L_n$ because the Lubin--Tate module $F$ was constructed from $\pi$: the endomorphism $[\pi]_F$ kills $F(n)$, and the Artin map is designed so that $\operatorname{Art}_K(\pi)|_{L_\infty} = \operatorname{id}$. So the kernel is $\langle \pi \rangle \cdot U_K^{(n)}$. 3. **Intersection.** $N(K_m L_n / K) = N(K_m/K) \cap N(L_n/K) = (\langle \pi^m \rangle \cdot U_K) \cap (\langle \pi \rangle \cdot U_K^{(n)})$. An element $\pi^a u$ lies in the intersection iff $m \mid a$ and $u \in U_K^{(n)}$, giving $\langle \pi^m \rangle \cdot U_K^{(n)}$. [/guided] [/step] [step:Show every finite abelian extension is contained in some $K_m L_n$] Let $M/K$ be a finite abelian extension. By the [Existence Theorem](/theorems/???), $M$ corresponds to its norm group $N(M/K)$, which is an open subgroup of finite index in $K^\times$. Since $K^\times \cong \pi^{\mathbb{Z}} \times U_K$ (every nonzero element of $K$ writes uniquely as $\pi^a u$ with $a \in \mathbb{Z}$, $u \in U_K$), an open subgroup of finite index in $K^\times$ contains $\pi^{m\mathbb{Z}} \times V$ for some $m \geq 1$ and some open subgroup $V$ of $U_K$ of finite index. Since $\{U_K^{(n)}\}_{n \geq 0}$ is a neighbourhood basis of $1$ in $U_K$ (the $I$-adic topology on $\mathcal{O}_K$ gives cosets of $1 + \pi^n\mathcal{O}_K = U_K^{(n)}$ as basic open neighbourhoods of $1$), the open subgroup $V$ contains $U_K^{(n)}$ for some $n \geq 1$. Therefore $N(M/K) \supset \langle \pi^m \rangle \cdot U_K^{(n)} = N(K_m L_n / K)$. By the inclusion-reversing correspondence of class field theory (the [Existence Theorem](/theorems/???)), $N(M/K) \supset N(K_m L_n / K)$ implies $M \subset K_m L_n$. [/step] [step:Conclude that $K^{\mathrm{ab}} = K^{\mathrm{ur}} L_\infty$] Every finite abelian extension $M/K$ is contained in $K_m L_n \subset K^{\mathrm{ur}} L_\infty$ for some $m, n$ (by the previous step). Since $K^{\mathrm{ab}}$ is the union (compositum) of all finite abelian extensions of $K$: \begin{align*} K^{\mathrm{ab}} = \bigcup_{M/K \text{ finite abelian}} M \subset K^{\mathrm{ur}} L_\infty. \end{align*} Conversely, $K^{\mathrm{ur}} L_\infty \subset K^{\mathrm{ab}}$ because both $K^{\mathrm{ur}}$ and $L_\infty$ are unions of finite abelian extensions of $K$: the unramified extensions $K_m / K$ are cyclic (with Galois group generated by Frobenius) and hence abelian, and the Lubin--Tate extensions $L_n / K$ are abelian (with $\operatorname{Gal}(L_n/K) \cong U_K/U_K^{(n)}$, which is abelian since $U_K$ is abelian). Their composita $K_m L_n$ are therefore abelian over $K$, so $K^{\mathrm{ur}} L_\infty = \bigcup_{m,n} K_m L_n \subset K^{\mathrm{ab}}$. Combining both inclusions: \begin{align*} K^{\mathrm{ab}} = K^{\mathrm{ur}} L_\infty. \end{align*} [guided] This is the fundamental theorem of local class field theory in its explicit form. The Lubin--Tate construction produces all totally ramified abelian extensions (via $L_\infty$), and the unramified extensions are produced by Frobenius lifts (via $K^{\mathrm{ur}}$). Together they generate all abelian extensions. The proof structure is: - **Containment $K^{\mathrm{ur}} L_\infty \subset K^{\mathrm{ab}}$**: immediate because each $K_m L_n$ is a finite abelian extension (compositum of abelian extensions of a local field is abelian since the Galois group embeds into the product of the individual Galois groups, which are abelian). - **Containment $K^{\mathrm{ab}} \subset K^{\mathrm{ur}} L_\infty$**: this is the hard direction. Given any finite abelian $M/K$, the Existence Theorem identifies $M$ with its norm group $N(M/K)$. Since $K^\times = \pi^{\mathbb{Z}} \times U_K$ and $N(M/K)$ is open of finite index, it contains $\pi^{m\mathbb{Z}} \times U_K^{(n)}$ for some $m, n$. But this is exactly $N(K_m L_n / K)$, and the inclusion-reversing Galois correspondence gives $M \subset K_m L_n$. Why does the Existence Theorem apply? It states that every open subgroup of finite index in $K^\times$ is a norm group of some finite abelian extension. Here we use the converse direction: the norm group of a finite abelian extension $M/K$ is open and of finite index, and the correspondence is inclusion-reversing. [/guided] [/step]