$\bar E=\bigcap_n \iota(E)U^{p^n}$ is closed in the semilocal units

Proved

Leopoldt.isClosed_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 $\iota:E=\mathcal O_K^\times\to U$ the diagonal embedding of the global units. Then the subgroup

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

(the platform's unitClosure p K) is a closed subgroup of $U$ .

Indeed each $\iota(E)\cdot U^{p^{n+1}}$ contains the open subgroup $U^{p^{n+1}}$ , so it is open, and an open subgroup of a topological group is closed; an intersection of closed sets is closed.

Preamble

import Definitions.Def_LeopoldtDefect

Formal statement

namespace Leopoldt

theorem isClosed_unitClosure (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K] :
    IsClosed (unitClosure p K : Set (SemilocalUnits p K)) := by sorry

end Leopoldt

Source

P. Mihăilescu, On CM ℤ_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, §1.1 (definition Ē = closure(ι(E)) = ⋂_{n>0} ι(E)·U^{p^n}); J. Neukirch, Algebraic Number Theory, Ch. II §5 (the p-adic logarithm/exponential and the multiplicative group of a p-adic field: for a p-adic field the subgroup of n-th powers of units is open)

View graph

Eˉ=⋂nι(E)Upn\bar E=\bigcap_n \iota(E)U^{p^n}Eˉ=⋂n​ι(E)Upn is closed in the semilocal units

$\bar E=\bigcap_n \iota(E)U^{p^n}$ is closed in the semilocal units