Leopoldt's conjecture iff the $p$ -adic logarithms of the units are $\mathbb Z_p$ -independent

Proved

Leopoldt.leopoldtConjecture_iff_linearIndependent_log

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

leopoldtnumber-theory

The $p$ -adic logarithm criterion for Leopoldt's conjecture. Let $p$ be a prime and $K$ a number field with unit group $E=\mathcal O_K^\times$ of $\mathbb Z$ -rank $r=r_1+r_2-1$ . For each prime $\mathfrak p\mid p$ of $\mathcal O_K$ let $K_{\mathfrak p}$ be the completion and let

\iota: E\to U=\prod_{\mathfrak p\mid p}\mathcal O_{\mathfrak p}^\times

be the diagonal embedding. Each $K_{\mathfrak p}$ is a $\mathbb Z_p$ -module via the canonical map $\mathbb Z_p\to K_{\mathfrak p}$ , and $\log_p$ denotes the $p$ -adic logarithm (Iwasawa's form $\log_p x=\lim_n (x^{p^n}-1)/p^n$ ).

Let $\eta_1,\dots,\eta_r\in E$ be units such that

the subgroup $\langle\eta_1,\dots,\eta_r\rangle$ has finite index in $E$ (so the $\eta_i$ are, up to finite index, a system of fundamental units; e.g. $\eta_i=\varepsilon_i^M$ for a fundamental system $\varepsilon_i$ ), and
every local image lies in the small ball: $|\iota(\eta_i)_{\mathfrak p}-1|_{\mathfrak p}\le |p|_{\mathfrak p}^2$ for all $i$ and all $\mathfrak p\mid p$ .

Then Leopoldt's conjecture holds for $K$ at $p$ (i.e. the Leopoldt defect $\mathcal D_L(K)=\operatorname{rk}_{\mathbb Z}E-\operatorname{rk}_{\mathbb Z_p}\overline{\iota(E)}$ vanishes) if and only if the vectors of $p$ -adic logarithms

\Big(\log_p \iota(\eta_i)_{\mathfrak p}\Big)_{\mathfrak p\mid p}\in\prod_{\mathfrak p\mid p}K_{\mathfrak p},\qquad i=1,\dots,r,

are linearly independent over $\mathbb Z_p$ .

This is the classical reformulation of Leopoldt's conjecture as the non-vanishing of the $p$ -adic regulator: the $\mathbb Z_p$ -rank of the closure $\overline{\iota(E)}$ equals the $\mathbb Z_p$ -rank of the $\mathbb Z_p$ -span of the logarithms of a basis of (a finite-index subgroup of) the units. It turns the topological rank condition in the definition of the defect into a linear-algebra condition on explicit $p$ -adic numbers.

Formalization Note. $K_{\mathfrak p}$ is v.1.adicCompletion K for v : Leopoldt.PrimesOver p K, with the platform's $\mathbb Z_p$ -algebra instance Leopoldt.instAlgebraPadicIntAdicCompletion; $\log_p$ is PadicLog.log, which on the ball $|x-1|\le|p|^2$ is an isometric homomorphism satisfying $\log_p(x^a)=a\log_p x$ for $a\in\mathbb Z_p$ . The ball hypothesis can always be achieved by replacing the $\eta_i$ with a common power.

Preamble

import Definitions.Def_PadicLog

open NumberField

Formal statement

namespace Leopoldt

theorem leopoldtConjecture_iff_linearIndependent_log (p : ℕ) [Fact p.Prime]
    (K : Type*) [Field K] [NumberField K] (η : Fin (Units.rank K) → (𝓞 K)ˣ)
    (hη : (Subgroup.closure (Set.range η)).FiniteIndex)
    (hball : ∀ (i : Fin (Units.rank K)) (v : PrimesOver p K),
      ‖((diagonalUnits p K (η i) v : v.1.adicCompletionIntegers K) : v.1.adicCompletion K) - 1‖
        ≤ ‖((p : ℕ) : v.1.adicCompletion K)‖ ^ 2) :
    LeopoldtConjecture p K ↔
      LinearIndependent ℤ_[p] (fun (i : Fin (Units.rank K)) (v : PrimesOver p K) =>
        PadicLog.log (p := p)
          ((diagonalUnits p K (η i) v : v.1.adicCompletionIntegers K) : v.1.adicCompletion K)) := by sorry

end Leopoldt

Source

L. C. Washington, Introduction to Cyclotomic Fields (2nd ed., GTM 83), §5.5 'The p-adic regulator' (definition of R_p(K) and the statement of Leopoldt's conjecture as R_p(K) ≠ 0, with its equivalence to rank_{Z_p} of the closure of the units being r_1+r_2-1); see also Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, Ch. X §3 'Leopoldt's conjecture'.

View graph

Leopoldt's conjecture iff the ppp-adic logarithms of the units are Zp\mathbb Z_pZp​-independent

Leopoldt's conjecture iff the $p$ -adic logarithms of the units are $\mathbb Z_p$ -independent