The principal semilocal units $U^{(1)}$ form an open subgroup of finite index in $U$

Proved

Leopoldt.isOpen_principalSemilocalUnits

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

leopoldtnumber-theoryp-adic

Let $K$ be a number field, $p$ a prime, and let

U=\prod_{\mathfrak p\mid p}\mathcal O_{\mathfrak p}^\times

be the group of semilocal units at $p$ (the platform's SemilocalUnits p K), with the product topology. Let

U^{(1)}=\{u\in U:\ \|u_{\mathfrak p}-1\|_{\mathfrak p}<1\ \text{for every }\mathfrak p\mid p\}=\prod_{\mathfrak p\mid p}U_{\mathfrak p}^{(1)}

be the subgroup of principal units (one-units). Then $U^{(1)}$ is a subgroup of $U$ which is open and of finite index.

Formally: there is a subgroup $H\le U$ whose members are exactly the $u$ with $\|u_{\mathfrak p}-1\|<1$ for all $\mathfrak p\mid p$ , and this $H$ is open and has finite index.

(In fact $U/U^{(1)}\cong\prod_{\mathfrak p\mid p}(\mathcal O_K/\mathfrak p)^\times$ , so the index is $\prod_{\mathfrak p\mid p}(N\mathfrak p-1)$ ; only finiteness is asserted here.)

Preamble

import Definitions.Def_PrimesOverNorm

Formal statement

namespace Leopoldt

theorem isOpen_principalSemilocalUnits (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K] :
    ∃ H : Subgroup (SemilocalUnits p K),
      (∀ u : SemilocalUnits p K, u ∈ H ↔ ∀ v : PrimesOver p K,
        ‖((u v : v.1.adicCompletionIntegers K) : v.1.adicCompletion K) - 1‖ < 1) ∧
      IsOpen (H : Set (SemilocalUnits p K)) ∧ H.FiniteIndex := by sorry

end Leopoldt

Source

J. Neukirch, Algebraic Number Theory, Ch. II §5, Prop. 5.3 (

\mathcal O^\times/U^{(n)}

finite,

U^{(n)}

open;

\mathcal O^\times/U^{(1)}\cong\kappa^\times

); P. Mihăilescu, arXiv:1105.4544, §1.1 (semilocal units

U

)

View graph

The principal semilocal units U(1)U^{(1)}U(1) form an open subgroup of finite index in UUU

The principal semilocal units $U^{(1)}$ form an open subgroup of finite index in $U$