$\bigcap_n \iota(E)U^{p^n} = \overline{\iota(E)} \vee \mu'(U)$

Proved

Leopoldt.unitClosure_eq_closure_sup_torsion

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

leopoldtnumber-theory

Let $p$ be a prime, $K$ a number field, $U$ the semilocal units at $p$ and $\iota:E\to U$ the diagonal embedding of the global units. Then, as subgroups of $U$ ,

\bigcap_{n\ge1}\iota(E)\,U^{p^{n}} \;=\; \overline{\iota(E)}\;\vee\;\mu'(U),

where $\overline{\iota(E)}$ is the topological closure of $\iota(E)$ in $U$ , and $\mu'(U)$ is the subgroup generated by (in fact equal to) the elements $t\in U$ with $t^m=1$ for some $m$ coprime to $p$ . This is the exact description of the group $\bar E$ used in the definition of the Leopoldt defect (the platform's unitClosure): it contains the closure of the global units and differs from it only by the finite prime-to- $p$ torsion of $U$ .

Preamble

import Definitions.Def_LeopoldtDefect

Formal statement

namespace Leopoldt
theorem unitClosure_eq_closure_sup_torsion (p : ℕ) [Fact p.Prime] (K : Type*) [Field K]
    [NumberField K] :
    unitClosure p K = (diagonalUnits p K).range.topologicalClosure ⊔
      Subgroup.closure {t : SemilocalUnits p K | ∃ m : ℕ, m.Coprime p ∧ t ^ m = 1} := by sorry
end Leopoldt

Source

P. Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, §1.1, p.3 (definition of Ē = ⋂_n ι(E)·U^{p^n}); J. Neukirch, Algebraic Number Theory, Ch. II, Prop. 5.7 (structure U ≅ μ_{q-1} × U^{(1)} of local units, U^{(1)} a finitely generated ℤ_p-module).

View graph

⋂nι(E)Upn=ι(E)‾∨μ′(U)\bigcap_n \iota(E)U^{p^n} = \overline{\iota(E)} \vee \mu'(U)⋂n​ι(E)Upn=ι(E)​∨μ′(U)

$\bigcap_n \iota(E)U^{p^n} = \overline{\iota(E)} \vee \mu'(U)$