Kernel of the semilocal $p$ -adic logarithm on principal semilocal units is the torsion

Proved

Leopoldt.semilocal_log_eq_zero_iff

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 $\mathfrak p\mid p$ of $\mathcal O_K$ let $K_{\mathfrak p}$ be the completion, $\mathcal O_{\mathfrak p}$ its ring of integers and $\log_p:U^{(1)}_{\mathfrak p}\to K_{\mathfrak p}$ the $p$ -adic logarithm on principal units. Let $U=\prod_{\mathfrak p\mid p}\mathcal O_{\mathfrak p}^\times$ be the semilocal units and let $u=(u_{\mathfrak p})\in U$ be a principal semilocal unit, i.e. $\|u_{\mathfrak p}-1\|_{\mathfrak p}<1$ for every $\mathfrak p\mid p$ . Then

\log_p u_{\mathfrak p}=0\ \text{for all }\mathfrak p\mid p\iff u^n=1\ \text{for some integer }n>0 .

In other words, the kernel of the semilocal logarithm $\mathrm{Log}_p=(\log_p)_{\mathfrak p\mid p}:\prod_{\mathfrak p\mid p}U^{(1)}_{\mathfrak p}\to\prod_{\mathfrak p\mid p}K_{\mathfrak p}$ is exactly the torsion subgroup. This is the input that turns Leopoldt's conjecture into a statement about the $p$ -adic rank of $\mathrm{Log}_p$ of the global units (the $p$ -adic regulator).

Formalization Note The semilocal units are Leopoldt.SemilocalUnits p K $=\prod_{v}(\mathcal O_v)^\times$ over Leopoldt.PrimesOver p K; the logarithm is PadicLog.log from Definitions.Def_PadicLog, applied coordinatewise in $K_v$ . The (true) fact that each completion has characteristic zero is taken as an instance argument [∀ v, CharZero (v.1.adicCompletion K)] because Mathlib does not register it as an instance; it can be supplied e.g. via charZero_of_injective_algebraMap.

Preamble

import Definitions.Def_PadicLog

Formal statement

namespace Leopoldt

theorem semilocal_log_eq_zero_iff (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K]
    [∀ v : PrimesOver p K, CharZero (v.1.adicCompletion K)]
    (u : SemilocalUnits p K)
    (hu : ∀ v : PrimesOver p K,
      ‖(((u v : (v.1.adicCompletionIntegers K)ˣ) : v.1.adicCompletionIntegers K) :
        v.1.adicCompletion K) - 1‖ < 1) :
    (∀ v : PrimesOver p K, PadicLog.log (p := p)
      (((u v : (v.1.adicCompletionIntegers K)ˣ) : v.1.adicCompletionIntegers K) :
        v.1.adicCompletion K) = 0) ↔ ∃ n : ℕ, 0 < n ∧ u ^ n = 1 := by sorry

end Leopoldt

Source

Washington, Introduction to Cyclotomic Fields (2nd ed., GTM 83), §5.1, Proposition 5.4 (the p-adic logarithm log_p on 1+pO extended to units; log_p(xy)=log_p x+log_p y; log_p x=0 iff x is a root of unity times a power of p) and Neukirch, Algebraic Number Theory, Ch. II, Prop. (5.4)–(5.5) (the logarithm on principal units U^(1), log x = lim (x^{p^n}-1)/p^n style extension). Iwasawa's limit form: Iwasawa, Lectures on p-adic L-functions, §2. Semilocal form: Washington §5.5 (p-adic regulator, Leopoldt's conjecture), Neukirch–Schmidt–Wingberg, Cohomology of Number Fields, §10.3.

View graph

Kernel of the semilocal ppp-adic logarithm on principal semilocal units is the torsion

Kernel of the semilocal $p$ -adic logarithm on principal semilocal units is the torsion