From the rank of the group matrix of $\log_p$ at one prime to $\mathbb{Z}_p$-independent semilocal logarithms of conjugates

This is the Galois-covariance step of Ax's deduction of Leopoldt's conjecture for totally real abelian fields: a rank bound for the group matrix of $p$-adic logarithms at one prime above $p$ yields $\mathbb{Z}_p$-linearly independent semilocal logarithm vectors.

Let $p$ be a prime and $K$ a totally real number field, Galois over $\mathbb{Q}$ with abelian Galois group $G$ of order $n = [K:\mathbb{Q}]$, so that $r = \operatorname{rank}\mathcal{O}_K^\times = n - 1$. Let $\varepsilon \in \mathcal{O}_K^\times$ be a unit all of whose conjugates $\sigma\varepsilon$ lie in the ball $\|x - 1\|_v \le \|p\|_v^2$ at every prime $v \mid p$ of $K$. For a unit $u$ write

for its semilocal $p$-adic logarithm vector. Fix a prime $v_0 \mid p$ and form the group matrix

all entries computed in $K_{v_0}$. The statement asserts: if $\operatorname{rank}_{K_{v_0}} A \ge n - 1$, then there are $r$ conjugates $\sigma_1\varepsilon, \dots, \sigma_r\varepsilon$ whose vectors

are linearly independent over $\mathbb{Z}_p$.

Proof route. Choose $r = n - 1$ rows of $A$ that are linearly independent over $K_{v_0}$, indexed by $\sigma_1, \dots, \sigma_r$. For $\tau \in G$ the automorphism $\tau$ induces an isometric isomorphism $K_{v_0} \to K_{\tau v_0}$ compatible with $\log_p$ and with the $\mathbb{Z}_p$-action, and Galois covariance of the semilocal logarithm gives $\log_p(\sigma_i\varepsilon)$ at $\tau v_0$ equal to $\tau$ applied to $\log_p(\tau^{-1}\sigma_i\varepsilon)$ at $v_0$. A $\mathbb{Z}_p$-relation $\sum_i c_i \Lambda(\sigma_i\varepsilon) = 0$, read at the primes $\tau v_0$, therefore gives $\sum_i c_i \log_p(\sigma_i\tau^{-1}\varepsilon) = 0$ in $K_{v_0}$ for every $\tau$ (here $G$ abelian is used), that is, a relation among the chosen rows with coefficients in $\mathbb{Z}_p \subset K_{v_0}$; so all $c_i = 0$.

Use. Together with Leopoldt.charSum_log_ne_zero_of_brumer, Matrix.card_sub_one_le_rank_of_charSum_ne_zero and Matrix.rank_map_le, which supply the rank bound, this proves Leopoldt.exists_linearIndependent_log_conj_of_brumer, whose conclusion is the one here; by Leopoldt.leopoldtConjecture_iff_exists_linearIndependent_log_conj that conclusion is Leopoldt's conjecture for $K$.

Formalization Note. The conclusion is verbatim that of Leopoldt.exists_linearIndependent_log_conj_of_brumer. The conjugate $\sigma\varepsilon$ is Units.map (RingOfIntegers.mapRingEquiv σ.toRingEquiv).toMonoidHom ε; $\Lambda$ is PadicLog.log applied to the components of Leopoldt.diagonalUnits; $n$ is Fintype.card (K ≃ₐ[ℚ] K) and $n - 1$ is truncated subtraction; the matrix is Matrix.of fun σ τ => log (... (σ * τ⁻¹) ...) with Matrix.rank over $K_{v_0}$. The Galois action on primes and completions is on the platform: Leopoldt.primesOverPerm, Leopoldt.GaloisAction.localRingEquiv and its continuity (Definitions.Def_LeopoldtGaloisAction), and the covariance theorem Leopoldt.log_diagonalUnits_conj, which is stated with RingOfIntegers.mapRingHom (σ : K →+* K) (equal to the mapRingEquiv form by ext). A proof also needs Leopoldt.units_rank_of_isTotallyReal, IsGalois.card_aut_eq_finrank, the $\mathbb{Z}_p$-linearity of a continuous ring homomorphism between completions (density of $\mathbb{Z}$ in $\mathbb{Z}_p$, in the pattern of Leopoldt.continuous_hom_zp_eq), and the extraction of $n - 1$ independent rows from the rank (Matrix.rank_eq_finrank_span_row, exists_linearIndependent_of_le_finrank). No finite-index hypothesis on $\varepsilon$ and no form of Brumer's theorem is assumed here.