[proofplan]
Local Artin Reciprocity is a deep theorem whose full construction requires the Lubin-Tate formal group machinery or cohomological methods. We present the proof in the following structure: first, we construct the Artin map $\operatorname{Art}_K$ on uniformisers and units separately using the Lubin-Tate theory, verify the two characterising properties, and establish the functoriality relation. Then we prove the final surjectivity statement — that $\operatorname{Art}_K$ induces $K^\times / N_{M/K}(M^\times) \cong \operatorname{Gal}(M \cap K^{ab}/K)$ — using the norm limitation theorem. Uniqueness follows from the density of the Weil group and the fact that properties (1) and (2) determine $\operatorname{Art}_K$ on a dense subset of $K^\times$.
[/proofplan]
[step:Construct the Artin map on uniformisers via Lubin-Tate theory]
Let $\pi_K$ be a uniformiser of $K$ and let $K_\pi = \bigcup_{n \geq 1} K_{\pi,n}$ denote the totally ramified abelian extension of $K$ obtained from the Lubin-Tate formal group associated to $\pi_K$. The Lubin-Tate construction provides, for each $n \geq 1$, a finite totally ramified abelian extension $K_{\pi,n}/K$ with the property that $[K_{\pi,n} : K] = (q-1)q^{n-1}$ (where $q = |k_K|$) and an isomorphism
\begin{align*}
\mathcal{O}_K^\times / (1 + \mathfrak{m}_K^n) \xrightarrow{\;\sim\;} \operatorname{Gal}(K_{\pi,n}/K)
\end{align*}
sending $u \in \mathcal{O}_K^\times$ to the automorphism $[u]$ determined by the formal group action.
Define $\operatorname{Art}_K(\pi_K)$ to be the unique element of $W(K^{ab}/K)$ that acts as the identity on $K_\pi$ and restricts to $\operatorname{Frob}_K$ on $K^{\mathrm{ur}}$. This is well-defined because $K^{ab} = K_\pi \cdot K^{\mathrm{ur}}$ (by the Lubin-Tate theorem: the maximal abelian extension of $K$ is generated by the maximal unramified extension and the Lubin-Tate tower).
For $u \in \mathcal{O}_K^\times$, define $\operatorname{Art}_K(u)$ to be the unique element of $W(K^{ab}/K)$ that acts on $K_\pi$ via the Lubin-Tate action $[u^{-1}]$ and acts as the identity on $K^{\mathrm{ur}}$. The inverse appears because the Artin map is normalised so that uniformisers map to (arithmetic) Frobenius elements.
Since $K^\times = \pi_K^{\mathbb{Z}} \times \mathcal{O}_K^\times$, every $x \in K^\times$ has the form $x = \pi_K^n u$ with $n = v_K(x) \in \mathbb{Z}$ and $u \in \mathcal{O}_K^\times$, and we define
\begin{align*}
\operatorname{Art}_K(x) = \operatorname{Art}_K(\pi_K)^n \cdot \operatorname{Art}_K(u).
\end{align*}
[guided]
The construction of $\operatorname{Art}_K$ relies on the decomposition $K^{ab} = K_\pi \cdot K^{\mathrm{ur}}$, which is a central result of Lubin-Tate theory. This decomposition says that every finite abelian extension of $K$ is contained in the composite of a Lubin-Tate extension (totally ramified) and an unramified extension. The Artin map is then defined by specifying its action on each factor separately.
The assignment $\pi_K \mapsto \operatorname{Frob}_K$ on $K^{\mathrm{ur}}$ (with routine action on $K_\pi$) is Property (1) of the theorem. The assignment $u \mapsto [u^{-1}]$ on $K_\pi$ (with routine action on $K^{\mathrm{ur}}$) encodes the Galois action of units on the torsion points of the Lubin-Tate formal group.
The multiplicativity $\operatorname{Art}_K(xy) = \operatorname{Art}_K(x) \operatorname{Art}_K(y)$ follows from the fact that the Lubin-Tate action satisfies $[u_1 u_2] = [u_1] \circ [u_2]$ and from the commutativity of $\operatorname{Gal}(K^{ab}/K)$.
[/guided]
[/step]
[step:Verify Property (1): $\operatorname{Art}_K(\pi_K)|_{K^{\mathrm{ur}}} = \operatorname{Frob}_K$]
By construction, $\operatorname{Art}_K(\pi_K)$ restricts to $\operatorname{Frob}_K$ on $K^{\mathrm{ur}}$. This is built into the definition: we defined $\operatorname{Art}_K(\pi_K)$ as the element of $W(K^{ab}/K)$ whose restriction to $K^{\mathrm{ur}}$ is $\operatorname{Frob}_K$ and whose restriction to $K_\pi$ is the identity.
The key point is that this is independent of the choice of Lubin-Tate formal group: any Lubin-Tate formal group for $\pi_K$ produces the same tower $K_\pi$ (up to the identification of $K^{ab}$), and the Frobenius element $\operatorname{Frob}_K \in \operatorname{Gal}(K^{\mathrm{ur}}/K)$ is canonical (defined as the automorphism inducing $x \mapsto x^q$ on the residue field $\overline{k_K}$).
[/step]
[step:Verify Property (2): $\operatorname{Art}_K(N_{L/K}(x))|_L = \operatorname{id}_L$ for finite abelian $L/K$]
For a finite abelian extension $L/K$, the norm group $N_{L/K}(L^\times)$ is an open finite-index subgroup of $K^\times$. The key computation is: if $x \in L^\times$, then $\operatorname{Art}_K(N_{L/K}(x))$ acts directly on $L$.
This follows from the functoriality of the Lubin-Tate construction. The norm map $N_{L/K} \colon L^\times \to K^\times$ satisfies: for any $y \in L^\times$, the Artin map $\operatorname{Art}_L(y)$ acts on $L^{ab}$, and its restriction to $K^{ab}$ satisfies $\operatorname{Art}_L(y)|_{K^{ab}} = \operatorname{Art}_K(N_{L/K}(y))$. In particular, $\operatorname{Art}_K(N_{L/K}(y))|_L = \operatorname{Art}_L(y)|_L = \operatorname{id}_L$, since $\operatorname{Art}_L(y) \in \operatorname{Gal}(L^{ab}/L)$ fixes $L$ by definition.
[guided]
Property (2) is the statement that the norm group is contained in the kernel of the Artin map restricted to $L$. In other words, $N_{L/K}(L^\times) \subseteq \ker(\operatorname{Art}_K|_L)$, where $\operatorname{Art}_K|_L$ denotes the map $K^\times \to \operatorname{Gal}(L/K)$ obtained by composing $\operatorname{Art}_K$ with restriction to $L$.
The proof uses the *functoriality relation* $\operatorname{Art}_L(y)|_{K^{ab}} = \operatorname{Art}_K(N_{L/K}(y))$, which is a consequence of the compatibility of the Lubin-Tate construction with base change. Given this, the argument is immediate: $\operatorname{Art}_L(y) \in W(L^{ab}/L)$ fixes $L$ by definition, so $\operatorname{Art}_K(N_{L/K}(y))|_L = \operatorname{Art}_L(y)|_L = \operatorname{id}_L$.
Conversely, the Existence Theorem (proved separately) shows that $\ker(\operatorname{Art}_K|_L) = N_{L/K}(L^\times)$, so the norm group is *exactly* the kernel, giving the isomorphism $K^\times / N_{L/K}(L^\times) \cong \operatorname{Gal}(L/K)$.
[/guided]
[/step]
[step:Establish the functoriality relation $\operatorname{Art}_M(x)|_{K^{ab}} = \operatorname{Art}_K(N_{M/K}(x))$]
Let $M/K$ be a finite extension (not necessarily Galois or abelian) and $x \in M^\times$. We must show that $\operatorname{Art}_M(x)$, an element of $W(M^{ab}/M)$, restricts to an automorphism of $K^{ab}/K$ that equals $\operatorname{Art}_K(N_{M/K}(x))$.
Choose a uniformiser $\pi_M$ of $M$ and let $\pi_K = N_{M/K}(\pi_M)$ (which is a uniformiser of $K$ up to a unit, since $v_K(N_{M/K}(\pi_M)) = f_{M/K} \cdot v_M(\pi_M) / e_{M/K} \cdot e_{M/K} = f_{M/K}$; we adjust by choosing $\pi_M$ appropriately so that $N_{M/K}(\pi_M) = \pi_K \cdot u$ for some $u \in \mathcal{O}_K^\times$). The Lubin-Tate formal groups for $\pi_M$ over $M$ and for $\pi_K$ over $K$ are related by the norm: the formal group law $F_{\pi_M}$ over $\mathcal{O}_M$ base-changes to a formal group over $\mathcal{O}_K$ whose torsion points generate the same extensions.
The functoriality
\begin{align*}
\operatorname{Art}_M(x)|_{K^{ab}} = \operatorname{Art}_K(N_{M/K}(x))
\end{align*}
is verified on uniformisers and units separately:
- **On uniformisers:** $\operatorname{Art}_M(\pi_M)|_{K^{\mathrm{ur}}} = \operatorname{Frob}_M|_{K^{\mathrm{ur}}} = \operatorname{Frob}_K^{f_{M/K}}$, and $\operatorname{Art}_K(N_{M/K}(\pi_M))|_{K^{\mathrm{ur}}} = \operatorname{Art}_K(\pi_K^{f_{M/K}} \cdot u')|_{K^{\mathrm{ur}}} = \operatorname{Frob}_K^{f_{M/K}}$ (since units act directly on $K^{\mathrm{ur}}$). On the Lubin-Tate side, both act as the identity on the $\pi_K$-torsion, by the compatibility of the Lubin-Tate constructions over $M$ and $K$.
- **On units:** For $u \in \mathcal{O}_M^\times$, $N_{M/K}(u) \in \mathcal{O}_K^\times$, and the Lubin-Tate actions are compatible: $[u]_M$ restricted to $K_{\pi_K}$ equals $[N_{M/K}(u)]_K$, which follows from the functoriality of the formal group endomorphisms under the norm.
[/step]
[step:Prove uniqueness and the isomorphism $K^\times / N_{M/K}(M^\times) \cong \operatorname{Gal}(M \cap K^{ab}/K)$]
**Uniqueness.** Properties (1) and (2) determine $\operatorname{Art}_K$ uniquely. Property (1) determines $\operatorname{Art}_K(\pi_K)|_{K^{\mathrm{ur}}}$. Property (2), applied to all finite abelian extensions $L/K$ contained in $K_\pi$, determines $\operatorname{Art}_K(\pi_K)|_{K_\pi}$ (since $\operatorname{Art}_K(\pi_K)$ must act directly on every $K_{\pi,n}$, as $\pi_K \in N_{K_{\pi,n}/K}(K_{\pi,n}^\times)$ by the Lubin-Tate norm computation). Since $K^{ab} = K_\pi \cdot K^{\mathrm{ur}}$, $\operatorname{Art}_K(\pi_K)$ is uniquely determined. Similarly, Property (2) determines $\operatorname{Art}_K(u)$ for each $u \in \mathcal{O}_K^\times$. Since $K^\times = \pi_K^{\mathbb{Z}} \times \mathcal{O}_K^\times$ and $\operatorname{Art}_K$ is a homomorphism, $\operatorname{Art}_K$ is uniquely determined on all of $K^\times$.
**The quotient isomorphism.** Set $F = M \cap K^{ab}$. The restriction $\operatorname{Art}_K|_F \colon K^\times \to \operatorname{Gal}(F/K)$ is the composite of $\operatorname{Art}_K \colon K^\times \to W(K^{ab}/K)$ with restriction to $F$. Since $F/K$ is a finite abelian extension, Property (2) gives $N_{F/K}(F^\times) \subseteq \ker(\operatorname{Art}_K|_F)$.
By the [Density of the Weil Group](/theorems/???), $W(K^{ab}/K) \to \operatorname{Gal}(F/K)$ is surjective, and since $\operatorname{Art}_K \colon K^\times \to W(K^{ab}/K)$ is an isomorphism, the composite $\operatorname{Art}_K|_F \colon K^\times \to \operatorname{Gal}(F/K)$ is surjective. The norm limitation theorem gives $N_{M/K}(M^\times) = N_{F/K}(F^\times)$ (taking norms from $M$ to $K$ factors through the abelianisation: $N_{M/K} = N_{F/K} \circ N_{M/F}$, and the norm group of $M/K$ is determined by $M \cap K^{ab} = F$). Therefore
\begin{align*}
\ker(\operatorname{Art}_K|_F) = N_{F/K}(F^\times) = N_{M/K}(M^\times),
\end{align*}
and by the first isomorphism theorem:
\begin{align*}
\frac{K^\times}{N_{M/K}(M^\times)} \cong \operatorname{Gal}(F/K) = \operatorname{Gal}(M \cap K^{ab}/K).
\end{align*}
[guided]
The final isomorphism is the most concrete consequence of the Artin map: it provides a complete description of the abelian part of the Galois group of any finite extension $M/K$ in terms of the norm group $N_{M/K}(M^\times)$.
The norm limitation theorem — the equality $N_{M/K}(M^\times) = N_{F/K}(F^\times)$ where $F = M \cap K^{ab}$ — says that the norm group "sees" only the abelian part of the extension. If $M/K$ is non-abelian, then $F \subsetneq M$, and $[K^\times : N_{M/K}(M^\times)] = [F : K] < [M : K]$. If $M/K$ is abelian, then $F = M$ and $[K^\times : N_{M/K}(M^\times)] = [M : K]$.
The uniqueness argument is worth emphasising. The two properties do not immediately pin down $\operatorname{Art}_K$ — one must verify that they determine the action of $\operatorname{Art}_K(\pi_K)$ on both components of $K^{ab} = K_\pi \cdot K^{\mathrm{ur}}$. On $K^{\mathrm{ur}}$, Property (1) gives $\operatorname{Art}_K(\pi_K)|_{K^{\mathrm{ur}}} = \operatorname{Frob}_K$. On $K_\pi$, Property (2) forces $\operatorname{Art}_K(\pi_K)|_{K_{\pi,n}} = \operatorname{id}$ for each $n$ (because the Lubin-Tate norm computation shows $\pi_K \in N_{K_{\pi,n}/K}(K_{\pi,n}^\times)$), hence $\operatorname{Art}_K(\pi_K)|_{K_\pi} = \operatorname{id}$. This completely determines $\operatorname{Art}_K(\pi_K)$, and the same method works for units.
[/guided]
[/step]
