This is already in Mathlib.

Recall from Galois theory that there is a normal basis for \(l\) over \(k\), i.e. a basis of the form

Define a map \(\mathrm{ind}_1(k) \cong l\) by

The map \(\Phi \) is clearly a linear bijection; we check that it commutes with the Galois action:

Let \(P\) be the maximal ideal of \({\mathcal O}_l\). Choose \(n\) such that \(P^n \subseteq U\). Choose a normal basis for \(l\) over \(k\) contained in \(P^n\) and let \(L\) be the span of that basis over \({\mathcal O}_k\). We therefore have an isomorphism of Galois modules \(L \cong \mathrm{ind}_1({\mathcal O}_k)\), and induced representations have trivial Tate cohomology.

Choose \(L \subseteq M\) as in lemma 80. Since \(L\) has finite index in \(M\) we have \(h(M) = h(L) = 1\).

Choose \(n\) large enough so that \(\exp (x)\) converges for all \(x \in P^n\), and such that all the terms \(x^r/r!\) are in \(P^n\) for \(r \ge 1\) and all the terms \(x^r / r!\) with \(r \ge 2\) have strictly larger valuation than that of \(x\). It is already proved in Mathlib that \(\exp (x+y)=\exp (x)\exp (y)\), and the fact that \(\exp \) commutes with the Galois action is straightforward. We’ll show that the map is a bijection from \(P^n\) to \(1+P^n\).

Suppose \(\exp (x)=1\) with \(x \in P^n\). If \(x \ne 0\) then \(x = \pi ^mu\) for some unit \(u\). By assumption on \(n\), \(\exp (x) = 1 + \pi ^m u + O(\pi ^{m+1})\); this gives a contradcition. Therefore the map \(\exp : P^n \to 1+P^n\) is injective.

One can show that the map \(P^n \to 1+P^n\) is surjective using Hensel’s lemma as follows. Choose \(y \in 1+P^n\). Then \(x_0 = y-1\) is in \(P^n\) and \(\exp (x) \equiv y \bmod P^{n+1}\). Furthermore \(\exp '(x_0) = \exp (x_0) \not\equiv 0 \bmod P\). Hensel’s lemma shows that there exists a solution to \(\exp (x)=y\) with \(x \equiv x_0 \bmod P^{n+1}\). In particular \(x \in P^n\).

Choose a subgroup \(1+P^n\) as in the 82. Since \({\mathcal O}_l^\times / (1+P^n)\) is finite we have (using 58 and 59)

The right hand side is \(1\) by 81.

We have a short exact sequence of representations

where the second map is the valuation. We’ve shown in 83, 57 that \(h(l/k,{\mathcal O}^\times )=1\) and \(h(l/k,{\mathbb Z}) = [l:k]\). Therefore \(h(l/k,l^\times ) = [l:k]\).

The follows from 84 and 78.

Let \(p\) be prime number dividing the degree \([l:k]\) and let \(k_p\) be the fixed field of a Sylow \(p\)-subgroup \(S_p\) of \(\mathrm{Gal}(l/k)\). By 48 and 49 it is sufficient to prove that \(|H^2(l/k_p,l^\times )| \le [l:k_p]\), which is a special case of the theorem. In the special case, the Galois group is \(S_p\), which is a solvable group. It is therefore sufficient to prove the theorem in the case that \(\mathrm{Gal}(l/k)\) is solvable. (Note that \(\mathrm{Gal}(l/k)\) is always solvable if \(l/k\) is an extension of local fields, but we do not need to prve this.)

We shall prove the theorem by induction on \(k\), starting with \(k=l\) and moving down in cyclic steps. The case \(k=l\) follows by 5. Assume the result for \(l/k\) and let \(k_0\) be a subfield of \(k\) with \(k/k_0\) cyclic. It follows from 78 that we have an inflation-restriction sequence in dimension 2:

The first term has order \([k : k_0]\) by 85, and the last term has order at most \([l:k]\) by the inductive hypothesis. Thereofore \(H^2( l/k_0, l^\times )\) has order at most \([l:k] \times [k : k_0] = [l: k_0]\).

In the case of \(l\), this follows from 79 as \(\mathrm{Gal}(l/k)\) may be identified with \(\mathrm{Gal}({\mathbb F}_l / {\mathbb F}_k)\), so we focus on the representation \(l^\times \). Given any subgroup \(S\) of the Galois group we must prove that \(H^\bullet _{\mathrm{Tate}}(l/m,l^\times ) \cong 0\), where \(m\) is the fixed field of \(S\).

Note that \(l/m\) is also unramified, so has cyclic Galois group. By 52, it’s suffient to prove that \(H^1(l/m,l^\times )\) and \(H^2(l/m,l^\times )\) are trivial. By 58 the representation \({\mathbb F}_l^\times \) has Herbrand quotient \(1\), so it’s enough to prove that \(H^1\) is trivial. This follows from 78.

By 79 we may choose \(x_0 \in {\mathbb F}_l\) such that \(\{ g \bullet x_0 :g \in \mathrm{Gal}(l/k)\} \) is a normal basis. Let \(y \in {\mathcal O}_l\) be a lift of \(x_0\). It follows from Nakayama’s lemma that \(\{ g \bullet y\} \) is a normal basis in \({\mathcal O}_l\). As in earlier proofs, this implies the isomorphism \({\mathcal O}_l \cong \mathrm{ind}_1 {\mathcal O}_k\).

Recall (82) that for \(n\) sufficiently large we have isomorphisms of Galois modules:

where the first map is the logarithm and the second map is multiplication by \(\pi _k^{-n}\). Hence by 88, the multiplictive subgroup \(1+P^n\) has trivial cohomology. The long exact sequence now gives isomorphisms

We’ll prove by induction on \(n\) that \({\mathcal O}_l^\times / (1+P^n)\) has trivial cohomology. In the case \(n = 1\) we have

In this case the result follows from 87.

For the inductive step we note that there is a short exact sequence of Galois modules

where we have identified \(P^n / P^{n+1}\) with \({\mathbb F}_l\). By the inductive hypothesis, we assume that \({\mathcal O}_l^\times / (1+P^n)\) has tivial cohomology. By 87 \({\mathbb F}_l\) has trivial cohomology. Hence by the long exact seqeunce, \({\mathcal O}_l^\times / (1+P^{n+1})\) has trivial cohomology.

This follows from the long exact sequence using 89.

This follows from 90 together with the description of \(H^2(l/k,{\mathbb Z})\) in 53.

This follows from 72 and 91.

Corollary of \(\mathrm{inv}_{\mathrm{Gal}(l/k)}(\sigma _{\mathrm{Gal}(l/k)}) = 1\) from 55.

Up to cohomology, \(\sigma _{l/k}\) does not depend on the choice of uniformizer, so we may assume \(\pi _k=\pi _l\) in our definitions of \(\sigma _{m/k}\) and \(\sigma _{m/l}\). We have \(F_l = F_k^f\) where \(f = [l:k]\). Hence

We shall write \(F_{m/k}\) and \(F_{l/k}\) for the Frobenius elements in \(\mathrm{Gal}(m/k)\) and \(\mathrm{Gal}(l/k)\) respectively. Note that \(F_{l/k}\) is the restriction of \(F_{m/k}\) to \(l\), so is the coset of \(F_{m/k}\) when we regard \(\mathrm{Gal}(l/k)\) as a quotient of \(\mathrm{Gal}(m/k)\). From the definition we have (for any \(\sigma \in H^2(l/k,l^\times )\)):

The terms in the sum are periodic since \(F_{l/k}^{[l:k]}=1\). This implies (by the tower law):

The right hand side is equal to \(\mathrm{inv}_{l/k}(\sigma )\). The formual \(\mathrm{infl}(\sigma _{l/k}) = [m:l]\cdot \sigma _{m/k}\) follows since both sides of the equation have local invariant equal to \(\frac{1}{[l:k]}\) (by 94).

From 78 we know that \(H^1(l/k,l^\times ) \cong 0\). From 86, we know that \(H^2(l/k,l^\times )\) has no more that \([l:k]\) elements. We have constructed an element \(\sigma _{l/k}\in H^2(l/k,l^\times )\) of order \([l:k]\), so \(H^2(l/k,l^\times )\) is cyclic of order \([l:k]\) and is generated by \(\sigma _{l/k}\).

This follows from 76 and 97.

This follows from 75.

Clearly if \(x \in N_{l/k}(l^\times )\) then \(x\) is a norm from both \(m_1\) and \(m_2\). Suppose conversely that \(x\) is a norm from both \(m_1\) and \(m_2\). Let \(S_i=\mathrm{Gal}(l/m_i)\) for \(i=1,2\). By the commutative diagram in 73, the coset \(xN(l^\times )\) is in the image of each \(S_i\) under the reciprocity map. Since the reciprocity map is bijective, \(xN(l^\times )\) is in the image of \(S_1 \cap S_2\). The condition \(l = m_1 m_2\) implies \(S_1 \cap S_2 = 1\). Therefore \(x \in N(l^\times )\).

By 89 we have \(H^0_{\mathrm{Tate}}(l/k,{\mathcal O}_l^\times ) \cong 0\), which implies that every element of \({\mathcal O}_k^\times \) is a norm. The element \(\pi _k^f\) is the norm of \(\pi _k\). Therefore \(\pi _k^{f{\mathbb Z}} \times {\mathcal O}_k^\times \subseteq N(l^\times )\). To prove equality, we note that these subgroups of \(k^\times \) have the same index. Indeed by 91, \(k^\times / N(l^\times )\) is isomorphic to \(\mathrm{Gal}(l/k)^\mathrm{ab}\), which has order \(f\).

Let \(m\) be the fixed field of \(I\). By 73 the image of \(I\) in \(k^\times / N(l^\times )\) is \(N_{m/k}(m^\times ) / N_{l/k}(l^\times )\). Since \(m/k\) is unramified, 101 implies

where \(f\) is the inertial degree of \(l/k\). If \(\pi _l\) is a uniformizer in \(l\) then \(N(\pi _l)\) is a unit multiple of \(\pi _k^f\). This implies

The result follows from this.

By Eisenstein’s criterion, the cyclotimic polynomial \(\Phi _{p^n}(X) = \frac{X^{p^n}-1}{X^{p^{n-1}}-1}\) is irreducible over \({\mathbb Q}_p\). Hence the degree of the extension is \(\phi (p^n)=p^n - p^{n-1}\). This coincides with the index:

It it therefore sufficient to prove that every element of \(p^{\mathbb Z}\times (1+p^n {\mathbb Z}_p)\) is a norm.

We have \(p = N(1-\zeta )\). It is therefore sufficient to show that every \(x \in 1 + p^n {\mathbb Z}_p\) is the norm of an element of \({\mathbb Z}_p[\zeta ]\). We split this into cases.

• Suppose \(p\) is an odd prime, so that \(\exp (pz)\) converges for all \(z\in {\mathbb Z}_p\). If \(a \in 1 +p^n{\mathbb Z}_p^\times \) then by 82 there is an expression of \(a\) of the form

  \[ a = \exp (p^n y), \qquad y \in {\mathbb Z}_p. \]

  It follows that

  \[ a= \exp (p\frac{y}{p-1}) ^{[{\mathbb Q}_p(\zeta ):{\mathbb Q}_p]} = N_{{\mathbb Q}_p(\zeta )/{\mathbb Q}_p}(\exp (py/(p-1))). \]

  In particular, \(x\in N({\mathbb Q}_p(\zeta )^\times )\).

• In the case \(p^n = 2\) we have \(l = {\mathbb Q}_2\), so every element of \({\mathbb Q}_2\) is a norm.

• In the case \(p=2\), \(n \ge 2\), there is an intermediate field \(l / {\mathbb Q}_2(i) / {\mathbb Q}_2\), and we have

  \[ N_{{\mathbb Q}_p(i) / {\mathbb Q}_p} (x+i y) = x^2 + y^2. \]

  It’s easy to show (for example using Hensel’s lemma) that if \(a \equiv 1 \bmod 4\) then \(a\) is the norm of an element of \({\mathbb Q}_p(i)\). If \(a \in 1 + 2^n {\mathbb Z}_2\) then we have for some \(b \in {\mathbb Z}_2\):

  \[ a = \exp (2^n b) = \exp (4b)^{[l:{\mathbb Q}_2(i)]}. \]

  The the exponential above converges to an element of \(1+4{\mathbb Z}_2\). In particular there is an element \(b \in {\mathbb Q}_2(i)\) such that

  \[ a = N_{{\mathbb Q}_2(i)/{\mathbb Q}_2} (b) ^[l:{\mathbb Q}_2(i)] = N_{l/{\mathbb Q}_2} (b) \]

The subgroup \(N_{l/{\mathbb Q}_p}(l^\times )\) is open in \({\mathbb Q}_p^\times \), so it must contain a subgroup of the form \(1+p^n{\mathbb Z}_p\) for some \(n\). Let \(f\) be the order of \(p\) in \({\mathbb Q}_p^\times / N(l^\times )\).

The subgroup \(p^{f{\mathbb Z}} \times {\mathbb Z}_p^\times \) is the norm subgroups for the unramified extension of degree \(f\), which is \({\mathbb Q}_p(\zeta _{p^f-1})\). The group \(p^{\mathbb Z}\times (1_p^n {\mathbb Z}_p)\) is the norm subgroup of \({\mathbb Q}_p(\zeta _{p^n})\). Hence \(l\) is contained in \({\mathbb Q}_p(\zeta _{p^f-1}, \zeta _{p^n})\).

Let \(S\) be a the set of primes which ramify in \(l\). For each \(p \in S\) we let \(\hat p\) be a prime of \(l\) above \(p\). We therefore have an abelian extension \(l_{\hat p} / {\mathbb Q}_p\). Choose \(r_p\) such that \(1+p^{r_p} {\mathbb Z}_p \subseteq N(l_{\hat p}^\times )\). Let \(n = \prod _{p \in S} p^{r_p}\). Let \(m = l(\zeta _n)\). We shall prove that \(m = {\mathbb Q}(\zeta _n)\), which implies \(l\) is isomorphic to a subfield of \({\mathbb Q}(\zeta _n)\).

For a prime \(p \in S\), let \(D_p\) and \(I_p\) be the decomposition subgroup and inertia subgroup of \(\mathrm{Gal}(m/{\mathbb Q})\) at \(p\). We may identify \(D_p\) with \(\mathrm{Gal}(m_p / {\mathbb Q}_p)\), and we have a reciprocity isomorphism

By 102 The image of \(I_p\) under the reciprocity map is

We have

Note that by 103, 73 and 102,

This implies \(N_{m_p/{\mathbb Q}_p} (m_p^\times ) \cap {\mathbb Z}_p^\times = 1+p^r {\mathbb Z}_p\). It follows that \(I_p \cong {\mathbb Z}_p^\times / (1+p^{r_p} {\mathbb Z}_p) \cong ({\mathbb Z}/ p^{r_p})^\times \). In particular \(|I_p| = \phi (p^{r_p})\), where \(\phi \) is the Euler totient function.

Let \(I\) be the subgroup generated by the \(I_p\) for \(p \in S\). The fixed field of \(I\) is an unramified extension of \({\mathbb Q}\), and is therefore equal to \({\mathbb Q}\). Therefore \(I = \mathrm{Gal}(m/{\mathbb Q})\) and we have

Hence \(m = {\mathbb Q}(\zeta _n)\).