[proofplan]
We prove the norm group identity $N(L/K) = N((L \cap K^{\mathrm{ab}})/K)$ and the index bound $(K^\times : N(L/K)) \leq [L:K]$ with equality iff $L/K$ is abelian. The argument uses the Local Artin Reciprocity isomorphism applied to the maximal abelian subextension $M = L \cap K^{\mathrm{ab}}$, which identifies $K^\times / N(M/K)$ with $\operatorname{Gal}(M/K)$. We then show $N(L/K) = N(M/K)$ and read off the index bound from $|\operatorname{Gal}(M/K)| = [M:K] \leq [L:K]$.
[/proofplan]
[step:Identify the maximal abelian subextension and apply Local Artin Reciprocity]
Set $M = L \cap K^{\mathrm{ab}}$, the maximal abelian subextension of $L/K$. Since $M/K$ is an abelian extension of local fields, the [Local Artin Reciprocity](/theorems/???) map gives an isomorphism:
\begin{align*}
\operatorname{Art}_K: K^\times / N(M/K) \xrightarrow{\;\sim\;} \operatorname{Gal}(M/K).
\end{align*}
In particular, $(K^\times : N(M/K)) = |\operatorname{Gal}(M/K)| = [M : K]$.
[guided]
The Local Artin Reciprocity theorem states that for any finite abelian extension $M/K$ of local fields, there is a canonical isomorphism $K^\times / N_{M/K}(M^\times) \cong \operatorname{Gal}(M/K)$. This is the core of local class field theory. The key property we use is that it identifies the norm subgroup $N(M/K)$ with the kernel of the Artin map, and the quotient $K^\times / N(M/K)$ has order equal to $[M:K]$.
[/guided]
[/step]
[step:Show $N(L/K) = N(M/K)$]
We prove both inclusions.
**$N(L/K) \subseteq N(M/K)$:** Since $M \subseteq L$, the norm satisfies the transitivity formula $N_{L/K} = N_{M/K} \circ N_{L/M}$. Therefore $N_{L/K}(L^\times) = N_{M/K}(N_{L/M}(L^\times)) \subseteq N_{M/K}(M^\times)$, giving $N(L/K) \subseteq N(M/K)$.
**$N(M/K) \subseteq N(L/K)$:** By the Artin reciprocity isomorphism, the norm group $N(M/K)$ is the kernel of the composition
\begin{align*}
K^\times \xrightarrow{\operatorname{Art}_K} \operatorname{Gal}(K^{\mathrm{ab}}/K) \twoheadrightarrow \operatorname{Gal}(M/K).
\end{align*}
The norm group $N(L/K)$ determines (via the Artin map) the Galois group of the maximal abelian subextension of $L/K$, which is $M = L \cap K^{\mathrm{ab}}$. By the universal property of the Artin map, $\operatorname{Art}_K(N(L/K))$ acts directly on $L \cap K^{\mathrm{ab}} = M$. Therefore $N(L/K) \subseteq \ker(\operatorname{Art}_K|_{\operatorname{Gal}(M/K)}) = N(M/K)$.
Combined with the first inclusion, $N(L/K) = N(M/K)$.
[guided]
The inclusion $N(M/K) \subseteq N(L/K)$ is the deeper direction and relies on the existence theorem in local class field theory: for every open subgroup of finite index $U \subseteq K^\times$, there exists a unique finite abelian extension $E/K$ with $N(E/K) = U$. Since both $N(L/K)$ and $N(M/K)$ correspond via the Artin map to the same abelian extension $M$ (because $M$ is the maximal abelian subextension of $L/K$), they must be equal.
More concretely: the Artin map sends $a \in K^\times$ to $\operatorname{Art}_K(a) \in \operatorname{Gal}(K^{\mathrm{ab}}/K)$. For $a \in N(L/K)$, write $a = N_{L/K}(b)$ for some $b \in L^\times$. The Artin map satisfies the compatibility $\operatorname{Art}_K(N_{L/K}(b))|_M = \operatorname{id}_M$ whenever $M \subseteq L \cap K^{\mathrm{ab}}$ (this is a consequence of the functoriality of the reciprocity map). Therefore $\operatorname{Art}_K(a)|_M = \operatorname{id}_M$, which means $a \in N(M/K)$.
[/guided]
[/step]
[step:Derive the index bound and characterise equality]
From $N(L/K) = N(M/K)$ and the Artin reciprocity isomorphism:
\begin{align*}
(K^\times : N(L/K)) = (K^\times : N(M/K)) = [M : K].
\end{align*}
Since $M = L \cap K^{\mathrm{ab}} \subseteq L$, we have $[M : K] \leq [L : K]$, giving the bound:
\begin{align*}
(K^\times : N(L/K)) \leq [L : K].
\end{align*}
**Equality holds iff $L/K$ is abelian:** Equality $(K^\times : N(L/K)) = [L : K]$ is equivalent to $[M : K] = [L : K]$, which (since $M \subseteq L$) is equivalent to $M = L$. But $M = L \cap K^{\mathrm{ab}} = L$ if and only if $L \subseteq K^{\mathrm{ab}}$, i.e., $L/K$ is abelian.
[/step]
