$\bar E$ is stable under $\mathbb Z_p$ -powers of principal units

Proved

Leopoldt.zpPow_mem_unitClosure

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

leopoldtnumber-theoryp-adic

Let $K$ be a number field, $p$ a prime, $U=\prod_{\mathfrak p\mid p}\mathcal O_{\mathfrak p}^\times$ the semilocal units at $p$ , and

\bar E=\bigcap_{n\ge0}\iota(E)\cdot U^{p^{n+1}}\le U

the $p$ -adic closure of the global units (the platform's unitClosure p K). Let $u\in\bar E$ be a principal unit, i.e. $\|u_{\mathfrak p}-1\|_{\mathfrak p}<1$ for every $\mathfrak p\mid p$ . Then for every $a\in\mathbb Z_p$ the element

u^a=\big(u_{\mathfrak p}^{\,a}\big)_{\mathfrak p\mid p},\qquad u_{\mathfrak p}^{\,a}=\lim_{n\to\infty}u_{\mathfrak p}^{\,a_n}\quad(a_n\in\mathbb N,\ a_n\to a),

is again a semilocal unit lying in $\bar E$ . Here $u_{\mathfrak p}^{\,a}$ is the $p$ -adic power OneUnits.zpPow of Def_OneUnits.

Formally: there exists $w\in\bar E$ whose $\mathfrak p$ -component is $\operatorname{zpPow}(u_{\mathfrak p},a)$ for every $\mathfrak p\mid p$ . In other words the principal part of $\bar E$ is a $\mathbb Z_p$ -submodule of $U^{(1)}$ .

Preamble

import Definitions.Def_PrimesOverNorm

Formal statement

namespace Leopoldt

theorem zpPow_mem_unitClosure (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K]
    (u : SemilocalUnits p K) (hu : u ∈ unitClosure p K)
    (h1 : ∀ v : PrimesOver p K,
      ‖((u v : v.1.adicCompletionIntegers K) : v.1.adicCompletion K) - 1‖ < 1)
    (a : ℤ_[p]) :
    ∃ w ∈ unitClosure p K, ∀ v : PrimesOver p K,
      ((w v : v.1.adicCompletionIntegers K) : v.1.adicCompletion K) =
        OneUnits.zpPow (p := p) ((u v : v.1.adicCompletionIntegers K) : v.1.adicCompletion K) a := by sorry

end Leopoldt

Source

P. Mihăilescu, On CM ℤ_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, §1.1 (Ē is a ℤ_p-module, ℤ_p-rank of Ē); J. Neukirch, Algebraic Number Theory, Ch. II §5, Prop. 5.5–5.7 (

U^{(1)}

is a

\mathbb Z_p

-module via

u^a=\lim u^{a_n}

)

View graph

Eˉ\bar EEˉ is stable under Zp\mathbb Z_pZp​-powers of principal units

$\bar E$ is stable under $\mathbb Z_p$ -powers of principal units