Leopoldt's conjecture as a $\mathbb{Z}_p$ -rank condition on the logarithms of any finite-index family of units

Proved

Leopoldt.leopoldtConjecture_iff_finrank_span_log

by xuanji · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

leopoldtnumber-theoryp-adic

Let $K$ be a number field, $p$ a prime, and for each prime $v\mid p$ of $K$ let $K_v$ be the completion and $\log_p:K_v\to K_v$ the $p$ -adic logarithm. Write

\Lambda(x)=\bigl(\log_p\iota_v(x)\bigr)_{v\mid p}\in\prod_{v\mid p}K_v

for the semilocal logarithm vector of a global unit $x$ ; $\prod_{v\mid p}K_v$ is a $\mathbb{Z}_p$ -module through the canonical maps $\mathbb{Z}_p\to K_v$ . Let $r=r_1+r_2-1$ be the unit rank.

Let $(u_i)_{i\in I}$ be a finite family of units of $\mathcal{O}_K$ generating a subgroup of finite index in $\mathcal{O}_K^\times$ , and assume that each $u_i$ lies in the logarithm ball at every $v\mid p$ :

\|\iota_v(u_i)-1\|_v\le\|p\|_v^{2}.

Then Leopoldt's conjecture holds for $(K,p)$ (i.e. the Leopoldt defect is $0$ ) if and only if

\operatorname{rank}_{\mathbb{Z}_p}\ \sum_{i\in I}\mathbb{Z}_p\,\Lambda(u_i)\;=\;r .

This generalises the criterion Leopoldt.leopoldtConjecture_iff_linearIndependent_log (which needs exactly $r$ units) to an arbitrary finite generating family of finite index, e.g. all Galois conjugates of a Minkowski unit, which satisfy one multiplicative relation (their norm is $\pm1$ ) and so are not independent. The rank is Module.finrank, which for the finitely generated torsion-free $\mathbb{Z}_p$ -module in question is its free rank. The ball hypothesis can always be achieved by replacing the units with a fixed power.

Preamble

import Definitions.Def_PadicLog

open NumberField

Formal statement

theorem Leopoldt.leopoldtConjecture_iff_finrank_span_log (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K] {ι : Type*} [Finite ι] (u : ι → (𝓞 K)ˣ)
    (hu : (Subgroup.closure (Set.range u)).FiniteIndex)
    (hball : ∀ (i : ι) (v : Leopoldt.PrimesOver p K),
      ‖((Leopoldt.diagonalUnits p K (u i) v : v.1.adicCompletionIntegers K) :
        v.1.adicCompletion K) - 1‖ ≤ ‖((p : ℕ) : v.1.adicCompletion K)‖ ^ 2) :
    Leopoldt.LeopoldtConjecture p K ↔
      Module.finrank ℤ_[p] (Submodule.span ℤ_[p] (Set.range fun (i : ι) (v : Leopoldt.PrimesOver p K) =>
        PadicLog.log (p := p)
          ((Leopoldt.diagonalUnits p K (u i) v : v.1.adicCompletionIntegers K) :
            v.1.adicCompletion K))) = NumberField.Units.rank K := by sorry

Source

L. C. Washington, Introduction to Cyclotomic Fields, 2nd ed., GTM 83, §5.5 (Leopoldt's conjecture; the p-adic regulator and the Z_p-rank of the closure of the units); J. Ax, On the units of an algebraic number field, Illinois J. Math. 9 (1965), 584–589, §1 (reformulation in terms of logarithms of a system of units of finite index).

View graph

Leopoldt's conjecture as a Zp\mathbb{Z}_pZp​-rank condition on the logarithms of any finite-index family of units

Leopoldt's conjecture as a $\mathbb{Z}_p$ -rank condition on the logarithms of any finite-index family of units