1 Setup
1.1 The fields and the primes
Let \(p\) be a prime number and \(f\) a positive integer. Set \(q = p^f\). Let \(L = \mathbb {Q}(\zeta _{p(q-1)})\) be the \(p(q-1)\)-th cyclotomic field. Inside \(L\), we consider the subfields \(K = \mathbb {Q}(\zeta _{q-1})\) and \(F = \mathbb {Q}(\zeta _p)\), and we fix a primitive \(p\)-th root of unity \(\zeta _p \in \mathcal{O}_F\). We fix a maximal ideal \(P\) of \(\mathcal{O}_K\) lying above \(p\) and a maximal ideal \(\mathfrak {P}\) of \(\mathcal{O}_L\) lying above \(P\). Since the order of \(p\) modulo \(q - 1\) is \(f\), the residue field \(\mathcal{O}_K/P\) has \(q\) elements.
In the formalization, most results of Chapters 1 to 3 are proved for an arbitrary integer \(n \geq 1\) in place of \(q - 1\), with \(K = \mathbb {Q}(\zeta _n)\), any number field \(L\) containing \(K\) and \(F\), and the hypothesis that \(P\) has Teichmüller lifts of order \(n\) (1). Some of them then carry hypotheses such as \(1 {\lt} n\), \(e(\mathfrak {P}\mid P) \geq 2\) or \(\zeta _p - 1 \notin \mathfrak {P}^2\), which all hold in the setting above. The case \(n = q - 1\) is obtained with 2.
1.2 The Teichmüller character
Let \(R\) be a commutative ring, \(I\) an ideal of \(R\) and \(n\) a positive integer. The ideal \(I\) has Teichmüller lifts of order \(n\) if the reduction map \(\mu _n(R) \to (R/I)^\times \) is bijective.
The ideal \(P\) has Teichmüller lifts of order \(q - 1\).
The ring \(\mathcal{O}_K\) contains \(q - 1\) distinct \((q-1)\)-th roots of unity, and the integer \(q - 1\) is not in \(P\). Hence these roots stay distinct modulo \(P\), so the reduction map is injective, and it is bijective since \((\mathcal{O}_K/P)^\times \) has \(q - 1\) elements.
Assume that \(P\) has Teichmüller lifts of order \(q - 1\) (2). The Teichmüller character \(\omega : \mathcal{O}_K/P \to \mathcal{O}_K\) is the multiplicative character whose restriction to \((\mathcal{O}_K/P)^\times \) is the inverse of the reduction map \(\mu _{q-1}(\mathcal{O}_K) \xrightarrow {\sim } (\mathcal{O}_K/P)^\times \), extended by \(\omega (0) = 0\).
For all \(x \in \mathcal{O}_K/P\), we have \(\omega (x) \equiv x \pmod{P}\).
This is the definition for \(x \neq 0\), and both sides vanish for \(x = 0\).
The order of \(\omega \) as a multiplicative character is \(q - 1\).
The values of \(\omega \) on units are \((q-1)\)-th roots of unity, so \(\omega ^{q-1} = 1\). The value of \(\omega \) at the reduction of a primitive \((q-1)\)-th root of unity is that root, so no smaller power of \(\omega \) is trivial.
Let \(a \in \mathbb {Z}\) with \((q-1) \nmid a\). The character \(\omega ^{-a}\), viewed with values in \(\mathcal{O}_L\), is nontrivial. In particular,
The character \(\omega ^{-a}\) is nontrivial by 5, and stays nontrivial after composing with the injection \(\mathcal{O}_K \to \mathcal{O}_L\). The vanishing of the sum is then MulChar.sum_eq_zero_of_ne_one.
Let \(R\) be a ring containing \(\mathcal{O}_K\) and let \(\sigma \) be a ring endomorphism of \(R\) such that \(\sigma (\zeta _{q-1}) = \zeta _{q-1}^m\) for some \(m \in \mathbb {N}\). Then \(\sigma (\omega (x)^a) = \omega (x)^{am}\) for all \(x \in \mathcal{O}_K/P\) and \(a \in \mathbb {Z}\).
For \(x \neq 0\), the value \(\omega (x)^a\) is a power \(\zeta _{q-1}^k\), so \(\sigma (\omega (x)^a) = \zeta _{q-1}^{mk} = \omega (x)^{am}\). Both sides vanish for \(x = 0\).
1.3 The additive character
The additive character \(\psi : \mathcal{O}_K/P \to \mathcal{O}_F\) is defined by
We also view it as a character with values in \(\mathcal{O}_L\).
The character \(\psi \) is nontrivial, i.e., \(\psi \neq 1\).
Since the extension \(\mathcal{O}_K/P\) over \(\mathbb {Z}/p\mathbb {Z}\) is separable, the trace \(\mathrm{tr}: \mathcal{O}_K/P \to \mathbb {Z}/p\mathbb {Z}\) is nonzero, so there exists \(x\) with \(\mathrm{tr}(x) \neq 0\), hence \(\psi (x) = \zeta _p^{\mathrm{tr}(x)} \neq 1\).
The character \(\psi \) is primitive.
Since \(\mathcal{O}_K/P\) is a field, any nontrivial additive character is primitive. The character \(\psi \) is nontrivial by 9.
For all \(x \in \mathcal{O}_K/P\), \(\psi (x^p) = \psi (x)\).
The Frobenius map \(x \mapsto x^p\) is a \((\mathbb {Z}/p\mathbb {Z})\)-algebra automorphism of \(\mathcal{O}_K/P\), so it preserves the trace.
Let \(\mathfrak {Q}\) be an ideal of \(\mathcal{O}_L\) with \(\zeta _p - 1 \in \mathfrak {Q}\). Then
for all \(x \in \mathcal{O}_K/P\).
Write \(\mathrm{tr}(x) = a\) with \(a \in \mathbb {N}\). By the binomial theorem, \(\psi (x) = (1 + (\zeta _p - 1))^a \equiv 1 + a(\zeta _p - 1) \pmod{\mathfrak {Q}^2}\).
Let \(\mathfrak {Q}\) be an ideal of \(\mathcal{O}_L\) with \(\zeta _p - 1 \in \mathfrak {Q}\). Then \(\psi (x) \equiv 1 \pmod{\mathfrak {Q}}\) for all \(x \in \mathcal{O}_K/P\).
This follows from 12, since \(\mathrm{tr}(x) \cdot (\zeta _p - 1) \in \mathfrak {Q}\).
1.4 Primes above \(p\)
For every prime ideal \(\mathfrak {Q}\) of \(\mathcal{O}_L\) above \(p\), we have \(\zeta _p - 1 \in \mathfrak {Q}\).
The ideal \((\zeta _p - 1)\) is the only prime of \(\mathcal{O}_F\) above \(p\), so it is \(\mathfrak {Q}\cap \mathcal{O}_F\).
Every prime ideal of \(\mathcal{O}_L\) above \(p\) is unramified over \(\mathcal{O}_F\).
Let \(\mathfrak {Q}\) be such a prime. By 105, \(e(\mathfrak {Q}\mid p) = p - 1\), and this is also the ramification index of \(p\) in \(F\). By multiplicativity of ramification indices in the tower \(L/F/\mathbb {Q}\), the ramification index of \(\mathfrak {Q}\) over \(\mathcal{O}_F\) is \(1\).