Nonvanishing of the nontrivial character sums of $\log_p$ of the conjugates of a Minkowski unit (Ax, from Brumer)

This is the Diophantine heart of Ax's deduction of Leopoldt's conjecture for totally real abelian fields from Brumer's theorem: the nontrivial character sums of the $p$-adic logarithms of the conjugates of a Minkowski unit do not vanish.

Let $p$ be a prime and $K$ a totally real number field, Galois over $\mathbb{Q}$ with Galois group $G$ of order $n = [K:\mathbb{Q}]$, so that $\operatorname{rank}\mathcal{O}_K^\times = n - 1$. Let $\varepsilon \in \mathcal{O}_K^\times$ be a unit whose conjugates $\sigma\varepsilon$ ($\sigma \in G$) generate a subgroup of finite index in $\mathcal{O}_K^\times$ (a Minkowski unit), and assume that every conjugate lies in the ball $\|x - 1\|_v \le \|p\|_v^2$ at every prime $v \mid p$ of $K$. Assume Brumer's theorem in the form: for every number field $L$, every prime $w \mid p$ of $L$ and every finite family of elements of $L$ lying in the ball at $w$, $\mathbb{Z}$-linear independence of their $p$-adic logarithms in $L_w$ implies $L$-linear independence.

Fix a prime $v \mid p$ of $K$ and write $\ell(\sigma) = \log_p(\sigma\varepsilon) \in K_v$. Let $L \supseteq K$ be a number field that contains a primitive $n$-th root of unity, let $w \mid p$ be a prime of $L$, and let $\iota : K_v \to L_w$ be a ring homomorphism compatible with the inclusions of $K$ into $K_v$ and of $K$ into $L \subseteq L_w$, with $\|\iota(x)\|_w = \|x\|_v^{\,c}$ for some real $c > 0$. Then for every nontrivial character $\chi : G \to L_w^\times$,

Proof route (Ax, Brumer). (1) The product of all conjugates is $N_{K/\mathbb{Q}}(\varepsilon) = \pm 1$; since $-1$ is outside the ball for every $p$ ($\|{-2}\| = 1$ for odd $p$, $\|2\| = \|p\| > \|p\|^2$ for $p = 2$) and the ball is a group, the norm is $1$ and $\sum_\sigma \ell(\sigma) = 0$. Hence the sum equals $\sum_{\sigma \ne 1} (\chi(\sigma) - 1)\,\iota(\ell(\sigma))$, and some coefficient $\chi(\sigma) - 1$ is nonzero. (2) The finite-index hypothesis and $\operatorname{rank}\mathcal{O}_K^\times = n - 1$ force the relation lattice $\{m \in \mathbb{Z}^G : \prod_\sigma (\sigma\varepsilon)^{m_\sigma} \text{ torsion}\}$ to have rank one, generated up to finite index by $(1, \dots, 1)$; so the $n - 1$ conjugates $\sigma\varepsilon$, $\sigma \ne 1$, are multiplicatively independent modulo torsion, and their logarithms in $L_w$ are $\mathbb{Z}$-linearly independent because $\log_p$ is injective on the ball and kills exactly the torsion there. (3) The values $\chi(\sigma)$ are $n$-th roots of unity in $L_w$; since $L$ contains a primitive one, they lie in $L$. (4) Brumer's theorem for $L$ at $w$ (with $\iota(\ell(\sigma)) = \log_p(\sigma\varepsilon)$ computed in $L_w$) gives $L$-linear independence of the $\log_p(\sigma\varepsilon)$, $\sigma \ne 1$, contradicting the relation in (1).

Use. With this nonvanishing, Dedekind's group matrix $(\iota(\ell(\sigma\tau^{-1})))_{\sigma,\tau}$ has rank at least $n - 1$ (Matrix.card_sub_one_le_rank_of_charSum_ne_zero), which is the input of Leopoldt.exists_linearIndependent_log_conj_of_card_sub_one_le_rank; together they prove Leopoldt.exists_linearIndependent_log_conj_of_brumer.

Formalization Note. The hypotheses hε, hball, hB are those of Leopoldt.exists_linearIndependent_log_conj_of_brumer, with hB the platform statement NumberField.Brumer.linearIndependent_log_algebraMap quantified over all number fields L in the universe of K; the field L of this statement lives in that same universe, so hB applies to it. Commutativity of $G$ is not assumed; the conjugate $\sigma\varepsilon$ is Units.map (RingOfIntegers.mapRingEquiv σ.toRingEquiv).toMonoidHom ε, and $\ell(\sigma)$ is PadicLog.log of its image in $K_v$ under Leopoldt.diagonalUnits. $n$ is Fintype.card (K ≃ₐ[ℚ] K). A proof will need: PadicLog.map_log (to identify $\iota(\ell(\sigma))$ with $\log_p$ in $L_w$ and to move the ball condition), Algebra.norm_eq_prod_automorphisms and Int.isUnit_iff for the norm relation, Leopoldt.units_rank_of_isTotallyReal and IsGalois.card_aut_eq_finrank for the rank, PadicLog.log_eq_zero_iff and PadicLog.log_injOn for the torsion step, and IsPrimitiveRoot.eq_pow_of_pow_eq_one for the pullback of character values.