The $\mathbb{Z}_p$ -rank of the semilocal units $U_p(\mathbb{F})$ is at most $[\mathbb{F} : \mathbb{Q}]$

Proved

Leopoldt.le_finrank_of_continuous_injective_semilocalUnits

by WCoram · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

local-fieldsnumber-theoryp-adicunits

Let $p$ be a prime and $\mathbb{F}$ a number field, and let $U_p(\mathbb{F}) = \prod_{\wp \mid p} \mathcal{O}_\wp^\times$ be its semilocal units at $p$ (Section 1.1 of the source). If

f : \mathbb{Z}_p^{\,n} \longrightarrow U_p(\mathbb{F})

is a continuous injective group homomorphism, then

n \le [\mathbb{F} : \mathbb{Q}] .

In other words, the free $\mathbb{Z}_p$ -rank of $U_p(\mathbb{F})$ , measured by continuous injections of $\mathbb{Z}_p^{\,n}$ as in the definition of zpRankBelow, is at most $[\mathbb{F} : \mathbb{Q}]$ . This is the standard structure of local units: for each $\wp \mid p$ the unit group $\mathcal{O}_\wp^\times$ is the product of a finite group and a copy of $\mathbb{Z}_p^{\,[\mathbb{F}_\wp : \mathbb{Q}_p]}$ (the principal units, via the $p$ -adic logarithm), and $\sum_{\wp \mid p} [\mathbb{F}_\wp : \mathbb{Q}_p] = [\mathbb{F} : \mathbb{Q}]$ . The source uses exactly this count when it takes $[\mathbb{F} : \mathbb{Q}]$ as the bound in the definition of the Leopoldt defect: the $\mathbb{Z}_p$ -rank of $\bar{E}(\mathbb{F})$ , a subgroup of $U_p(\mathbb{F})$ , never exceeds $[\mathbb{F} : \mathbb{Q}]$ , so the bound argument of zpRankBelow never truncates. It is needed whenever a continuous injection $\mathbb{Z}_p^{\,n} \hookrightarrow \bar{E}(\mathbb{F})$ produced by an argument has to be fed back into zpRankBelow p (finrank ℚ F) (unitClosure p F), which requires the witness $n$ to satisfy this bound.

Formalization Note $\mathbb{Z}_p^{\,n}$ is Multiplicative (Fin n → ℤ_[p]) with the product topology, and continuity is with respect to the product topology on SemilocalUnits p F, exactly as in zpRankBelow. Only the inequality is asserted; the full structure of $\mathcal{O}_\wp^\times$ is not part of the statement.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem le_finrank_of_continuous_injective_semilocalUnits (p : ℕ) [Fact p.Prime]
    (F : Type*) [Field F] [NumberField F] {n : ℕ}
    (f : Multiplicative (Fin n → ℤ_[p]) →* SemilocalUnits p F)
    (hf : Function.Injective f) (hc : Continuous f) :
    n ≤ Module.finrank ℚ F := by sorry
end Leopoldt

Source

Preda Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544 (v4, 17 Feb 2016), Section 1.1, p. 3, definition of the Z_p-rank of Ebar inside U = prod_{wp|p} O_wp^x, together with the standard fact (e.g. J. Neukirch, Algebraic Number Theory, Springer 1999, Chapter II, Proposition 5.7, and Theorem 8.3 for the decomposition K tensor Q_p = prod K_wp) that O_wp^x is the product of a finite group and Z_p^{[F_wp : Q_p]} and that sum_{wp | p} [F_wp : Q_p] = [F : Q]. The definition file Def_LeopoldtDefect records this bound in its docstring for zpRankBelow ("The Z_p-rank of Ebar is bounded by that of the whole semilocal unit group U, which is [K : Q]").

View graph

The Zp\mathbb{Z}_pZp​-rank of the semilocal units Up(F)U_p(\mathbb{F})Up​(F) is at most [F:Q][\mathbb{F} : \mathbb{Q}][F:Q]

The $\mathbb{Z}_p$ -rank of the semilocal units $U_p(\mathbb{F})$ is at most $[\mathbb{F} : \mathbb{Q}]$