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 \(f_0\) be a \(q+1\)-cocycle with values in \(M=M_0\). Since \(H^{q+1}(G,M/M_1)=0\) we can find a \(q\)-cochain \(\psi _0\) of \(G\) with values in \(M\) such that \(f_0=\delta \psi _0+f_1\) where now \(f_1\) is a \(q+1\)-cocycle in \(M_1\). In general given the \(q+1\)-cocycle \(f_n\) with values in \(M_n\) we recursively define a \(q\)-chain \(\psi _n\) with values in \(M_n\) such that \(f_n=\delta \psi _n+f_{n+1}\) with \(f_{n+1}\) a \(q+1\)-cocycle taking values in \(M_{n+1}\). Now set \(\psi :=\psi _0+\psi _1+\cdots \), which converges by our hypothesis \(M=\varprojlim (M/M_i)\). More precisely, \(\psi \) can be thought of as an element of the projective limit of \(C^q(M/M_i)\), which equals \(C^q(M)\). In particular \(\psi \) defines a \(q\)-cochain of \(G\) with values in \(M\); an elementary calculation now shows \(f_0=\delta \psi \) and thus \(f_0\) is a coboundary.

We know that \(l\cong k[G]\) by the normal basis theorem so we may choose \(\alpha \in L\) such that \(\{ g\alpha :g\in G\} \) forms a \(k\)-basis for \(l\). If \(\pi _k\) denotes a uniformiser of \(k\) then by multiplying \(\alpha \) by an appropriate power of \(\pi _k\) we may assume \(\alpha \in {\mathcal O}_l\). Set \(A=\oplus _{g\in G}{\mathcal O}_k g\alpha \subseteq {\mathcal O}_l\). This is an open additive subgroup of \(l\) so there exists some natural \(N\) such that \(\pi _k^N{\mathcal O}_l\subseteq A\). Set \(B=\pi _k^{N+1}A\subseteq \pi _k{\mathcal O}_l\) and set \(M=1+B\subseteq {\mathcal O}_l^\times \). We claim that this \(M\) works. It is clearly open and \(G\)-stable, so what remains is \(H^{q+1}(l/k,M)=0\) for all naturals \(q\).

First observe that \(B\cdot B\subseteq \pi _kB\), as \(B\cdot B\subseteq \pi _k^{2N+2}A\cdot A \subseteq \pi _k^{2N+2}{\mathcal O}_l\subseteq \pi _k^{N+2}A=\pi _kB.\) Now define subgroups \(M_i=1+\pi _k^iB\); we claim that lemma 80 applies for all \(q\). To check this, we need to show that \(H^{q+1}(G,M_i/M_{i+1})=0\) for all \(i\). But it is not difficult to check that the map \(M_i\to B\) sending \(1+\pi _k^ib\) to \(b\) induces a \(G\)-equivariant isomorphism \(M_i/M_{i+1}=B/\pi _kB\) (the case \(i=0\) needs \(B\cdot B\subseteq \pi _kB\)), and the latter has trivial cohomology because it is isomorphic to \(({\mathcal O}_k/\pi _k)[G]\) and thus induced.

Choose a subgroup \(M\subseteq {\mathcal O}_l^\times \) as in Lemma 81. Since \({\mathcal O}_l^\times / M\) is finite (because \(M\) is open and \({\mathcal O}_l^\times \) is compact) we have (using lemmas 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 82, 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 83 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 prove 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 84, and the last term has order at most \([l:k]\) by the inductive hypothesis. Therefore \(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 sufficient 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\).

Because replacing \(Gal(l/k)\) with a subgroup is the same as replacing \(k\) with an extension, it suffices to prove that \(H^{q+1}(l/k,{\mathcal O}_l^\times )=0\) for all local fields \(k\), unramified extensions \(l\) and naturals \(q\). Filter \({\mathcal O}_l^\times \) as \({\mathcal O}_l^\times \supset 1+\pi _k{\mathcal O}_l\supset 1+\pi _k^2{\mathcal O}_l\supset \cdots \). By lemma 80 it suffices to prove that all the subquotients have trivial cohomology. However the first subquotient is \({\mathbb F}_l^\times \) and all the others are \({\mathbb F}_l\), so it suffices to prove that \(H^q(G,{\mathbb F}_l^\times )\cong H^q(G,{\mathbb F}_l)\cong 0\) for all \(q\geq 1\). But these follow from lemma 86.

This follows from the long exact sequence using 88.

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

This follows from 72 and 90.

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 formula \(\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 93).

From 78 we know that \(H^1(l/k,l^\times ) \cong 0\). From 85, we know that \(H^2(l/k,l^\times )\) has no more than \([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 96.

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 88 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 90, \(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, 100 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.

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 contradiction. 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\).

By Eisenstein’s criterion, the cyclotomic 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 102 (with \(l=k={\mathbb Q}_p\)) 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 101 The image of \(I_p\) under the reciprocity map is

We have

Note that by 103, 73 and 101,

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)\).