The Leopoldt defect $\mathcal{D}_L(\mathbb{K})$ of a number field at $p$

Definition

LeopoldtDefect

by kbuzzard · Sep 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

iwasawa-theorynumber-theoryp-adicunits

This file sets up the objects that the statement of Leopoldt's conjecture refers to, following Section 1.1 of the source.

Let $p$ be a prime and let $\mathbb{K}$ be a number field with ring of integers $\mathcal{O}(\mathbb{K})$ and unit group $E = \mathcal{O}(\mathbb{K})^\times$ . Four objects are defined.

The primes above $p$ . $P = \{\wp \subset \mathcal{O}(\mathbb{K}) : (p) \subset \wp\}$ , the set of non-zero prime ideals of $\mathcal{O}(\mathbb{K})$ containing $p$ . This set is finite, and the finiteness is recorded so that it can be used as an instance.
The semilocal units. For $\wp \in P$ let $\mathbb{K}_\wp$ be the completion of $\mathbb{K}$ at $\wp$ and $\mathcal{O}_\wp \subset \mathbb{K}_\wp$ its valuation ring. The group of semilocal units at $p$ is the product of the local unit groups,

U \;=\; \prod_{\wp \in P} \mathcal{O}_\wp^{\times},

a commutative topological group. The diagonal embedding $\iota : E \to U$ sends a global unit to the tuple of its images under the completion maps.

The $p$ -adic closure of the global units. With $U^{p^n} = \{u^{p^n} : u \in U\}$ , and writing the product of two subgroups of the abelian group $U$ for their join,

\bar{E} \;=\; \bigcap_{n > 0} \iota(E) \cdot U^{p^n} \;\subseteq\; U .

The Leopoldt defect. Writing $\mathbb{Z}\text{-rk}(E) = r_1 + r_2 - 1$ for Dirichlet's unit rank and $\mathbb{Z}_p\text{-rk}(\bar{E})$ for the free $\mathbb{Z}_p$ -rank of $\bar{E}$ ,

\mathcal{D}_L(\mathbb{K}) \;=\; \mathbb{Z}\text{-rk}(E) \;-\; \mathbb{Z}_p\text{-rk}(\bar{E}).

Leopoldt's conjecture for $\mathbb{K}$ at $p$ is the assertion $\mathcal{D}_L(\mathbb{K}) = 0$ ; the defect is positive exactly when units independent over $\mathbb{Z}$ become dependent $p$ -adically after the diagonal embedding. For CM fields a positive defect is equivalent to the vanishing of the $p$ -adic regulator.

These are the objects every statement in this mission is phrased in, so they fix the meaning of the goal theorem. They are also reusable for any $p$ -adic question about global units: the semilocal unit group and the diagonal embedding are the standard setting for $p$ -adic regulators, $p$ -ramified class field theory, and the $\mathbb{Z}_p$ -rank computations of Iwasawa theory.

Formalization Note Four conventions are fixed here. First, $\bar{E}$ is defined by the displayed intersection rather than as a topological closure; the source gives both descriptions, and the intersection avoids committing to a topology on $\prod_\wp \mathbb{K}_\wp$ . The two can differ by a finite subgroup, which does not change the $\mathbb{Z}_p$ -rank.

Second, the free $\mathbb{Z}_p$ -rank of a subgroup $H$ is defined as the largest $n$ below a cut-off admitting a continuous injective homomorphism $\mathbb{Z}_p^n \to H$ , the cut-off being taken to be $[\mathbb{K}:\mathbb{Q}]$ when the defect is formed. Continuity is essential, since as abstract groups $\mathbb{Z}_p^n$ embeds into $\mathbb{Z}_p$ for every $n$ ; and because $\mathbb{Z}_p^n$ is compact and the ambient group Hausdorff, such an injection is automatically a closed embedding. For a closed subgroup of $U$ , isomorphic to a finite group times $\mathbb{Z}_p^d$ , such injections exist exactly for $n \le d$ . The cut-off is present only so that the supremum ranges over a visibly bounded set of naturals and never returns the junk value of a supremum of an unbounded set; since the $\mathbb{Z}_p$ -rank of $U$ itself is $[\mathbb{K}:\mathbb{Q}]$ , it never binds.

Third, the subtraction defining the defect is truncated subtraction of natural numbers; since the $\mathbb{Z}_p$ -rank never exceeds the $\mathbb{Z}$ -rank this is never triggered, and vanishing of the defect is equivalent to equality of the two ranks.

Fourth, the auxiliary constructions leading up to the defect are stated for an arbitrary natural number $p$ , primality being assumed only where it is used, so they also carry (unused) meaning at $p = 0$ and $p = 1$ .

Definition code

import Mathlib

/-!
# The Leopoldt defect of a number field at a prime `p`

This file formalises the objects of Section 1.1 ("Notations and fundamental facts") of

  Preda Mihăilescu, *On CM `ℤ_p`-extensions and the Leopoldt conjecture for CM fields*,
  arXiv:1105.4544,

which are what the statement of its Theorem 1 refers to.

Following the paper: `E = E(K) = 𝓞(K)ˣ` denotes the units of a number field `K`, and
`P = {℘ ⊂ 𝓞(K) : (p) ⊂ ℘}` the set of primes above `p`.  The paper puts
`K_p = ∏_{℘ ∈ P} K_℘ = K ⊗_ℚ ℚ_p`, lets `ι : K → K_p` be the diagonal embedding and
`U ⊂ K_p^×` be "the group of units, thus the product of local units at the same
completions".  It then defines the `p`-adic closure of the global units as

  `Ē = closure(ι(E)) = ⋂_{n > 0} ι(E) · U^{p^n}`

and the *Leopoldt defect* as

  `𝒟_L(K) = ℤ-rk(E) - ℤ_p-rk(Ē)`.

Leopoldt's conjecture for `K` at `p` is the assertion `𝒟_L(K) = 0`.
-/

namespace Leopoldt

open NumberField IsDedekindDomain

variable (p : ℕ) [Fact p.Prime] (K : Type*) [Field K] [NumberField K]

/-- The set `P = {℘ ⊂ 𝓞(K) : (p) ⊂ ℘}` of primes of `𝓞 K` above `p`. -/
abbrev PrimesOver := {v : HeightOneSpectrum (𝓞 K) // (p : 𝓞 K) ∈ v.asIdeal}

instance : Finite (PrimesOver p K) := by
  have hpne : (p : 𝓞 K) ≠ 0 := Nat.cast_ne_zero.2 (Fact.out (p := p.Prime)).ne_zero
  have hp0 : Ideal.span {(p : 𝓞 K)} ≠ 0 := by
    simpa [Ideal.span_singleton_eq_bot] using hpne
  apply Set.Finite.to_subtype
  refine (Ideal.finite_factors (R := 𝓞 K) hp0).subset ?_
  intro v hv
  exact Ideal.dvd_iff_le.2 ((Ideal.span_singleton_le_iff_mem _).2 hv)

/-- `U`: the group of semilocal units at `p`, that is the product `∏_{℘ | p} 𝓞_℘^×` of the
local units at the primes above `p`. -/
abbrev SemilocalUnits := ∀ v : PrimesOver p K, (v.1.adicCompletionIntegers K)ˣ

/-- `ι : E(K) → U`, the diagonal embedding of the global units into the semilocal units. -/
noncomputable def diagonalUnits : (𝓞 K)ˣ →* SemilocalUnits p K :=
  MonoidHom.pi fun v => Units.map (algebraMap (𝓞 K) (v.1.adicCompletionIntegers K)).toMonoidHom

/-- `Ē = ⋂_{n > 0} ι(E) · U^{p^n}`, the `p`-adic closure of the image of the global units
inside the semilocal units, exactly as the intersection is written in the source. -/
noncomputable def unitClosure : Subgroup (SemilocalUnits p K) :=
  ⨅ n : ℕ, ((diagonalUnits p K).range ⊔ (powMonoidHom (p ^ (n + 1))).range)

/-- The free `ℤ_p`-rank of a subgroup `H` of a commutative topological group, computed as the
largest `n ≤ bound` for which `ℤ_p^n` admits a continuous injective homomorphism into `H`.

For a closed subgroup of the semilocal units this is the usual free `ℤ_p`-rank: such a subgroup
is isomorphic to `Δ × ℤ_p^d` with `Δ` finite, and continuous injections from `ℤ_p^n` exist
exactly for `n ≤ d`.  Continuity is essential — as abstract groups `ℤ_p^n` embeds into `ℤ_p`
for every `n`; and since `ℤ_p^n` is compact and the target Hausdorff, a continuous injection is
automatically a closed embedding.

The `bound` is carried only so that the supremum is visibly taken over a bounded set and never
falls back on the junk value of `sSup` on an unbounded set of naturals.  Any `bound` at least as
large as the true rank yields the true rank. -/
noncomputable def zpRankBelow {G : Type*} [CommGroup G] [TopologicalSpace G]
    (bound : ℕ) (H : Subgroup G) : ℕ :=
  sSup {n : ℕ | n ≤ bound ∧ ∃ f : Multiplicative (Fin n → ℤ_[p]) →* G,
    Function.Injective f ∧ Continuous f ∧ ∀ x, f x ∈ H}

/-- The **Leopoldt defect** `𝒟_L(K) = ℤ-rk(E) - ℤ_p-rk(Ē)` of `K` at `p`.

`ℤ-rk(E) = r₁ + r₂ - 1` is Dirichlet's unit rank, which Mathlib provides as
`NumberField.Units.rank`.  The `ℤ_p`-rank of `Ē` is bounded by that of the whole semilocal unit
group `U`, which is `[K : ℚ]`, so taking `[K : ℚ]` as the bound never constrains it. -/
noncomputable def defect : ℕ :=
  Units.rank K - zpRankBelow p (Module.finrank ℚ K) (unitClosure p K)

/-- **Leopoldt's conjecture** for `K` at `p`: the Leopoldt defect vanishes. -/
def LeopoldtConjecture : Prop := defect p K = 0

end Leopoldt

Source

Preda Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544, Section 1.1 'Notations and fundamental facts' (pp. 2-3): the definitions of E(K), the set P of primes above p, K_p = prod_{wp in P} K_wp = K (x)_Q Q_p, the diagonal embedding iota, the semilocal units U, the p-adic closure Ebar = closure(iota(E)) = intersection_{n>0} iota(E).U^{p^n}, and the Leopoldt defect D_L(K) = Z-rk(E) - Z_p-rk(Ebar).

Read-back

What the Lean code literally says, in plain math · claude-opus-5

`PrimesOver`

For a natural number $p$ carrying the assumption that $p$ is prime, and a field $K$ carrying the assumption that $K$ is a number field (a finite-dimensional field extension of $\mathbb{Q}$ ), $\mathrm{PrimesOver}(p, K)$ is defined to be the type of pairs consisting of a point $v$ of the height-one spectrum of the ring of integers $\mathcal{O}_K$ — that is, a nonzero prime ideal $\mathfrak{p}_v \subseteq \mathcal{O}_K$ (the height-one spectrum of a Dedekind domain packages an ideal together with proofs that it is prime and nonzero) — together with a proof that the image of $p$ under the canonical map $\mathbb{N} \to \mathcal{O}_K$ lies in $\mathfrak{p}_v$ . So its elements are exactly the nonzero primes of $\mathcal{O}_K$ containing $p$ , i.e. the primes of $K$ dividing $p$ . It is introduced as a reducible abbreviation, and $p$ and $K$ are explicit parameters; the primality of $p$ enters only through the ambient hypothesis and is not used in the defining condition itself, which is literally just " $p \in \mathfrak{p}_v$ ".

The finiteness instance for `PrimesOver`

A typeclass instance is registered asserting that, under the same hypotheses ( $p$ prime, $K$ a number field), the type $\mathrm{PrimesOver}(p, K)$ of nonzero primes of $\mathcal{O}_K$ containing $p$ is a finite type. This is a statement of finiteness only; it provides no cardinality, no lower bound, and no claim that the type is nonempty (although for a prime $p$ it is in fact nonempty, nothing here says so).

`SemilocalUnits`

Under the same hypotheses, $\mathrm{SemilocalUnits}(p, K)$ is defined (again as a reducible abbreviation) to be the type of all functions assigning to each $v \in \mathrm{PrimesOver}(p, K)$ an element of the unit group $\mathcal{O}_{K_v}^{\times}$ , where $\mathcal{O}_{K_v}$ denotes the ring of integers of the $v$ -adic completion of $K$ — concretely, the valuation subring $\{x \in K_v : |x|_v \le 1\}$ of the completion $K_v$ of $K$ at the prime $\mathfrak{p}_v$ . Thus

\mathrm{SemilocalUnits}(p,K) \;=\; \prod_{v \mid p} \mathcal{O}_{K_v}^{\times},

the full unit group of the semilocal ring, taken as an unrestricted product over the (finitely many) primes above $p$ . It is the whole unit group of each local ring of integers: no restriction to principal units, one-units, or any congruence subgroup is imposed. Its group structure is the pointwise one (a commutative group, since each $\mathcal{O}_{K_v}$ is a commutative ring), and its topology is the product of the topologies each $\mathcal{O}_{K_v}^{\times}$ inherits from $\mathcal{O}_{K_v}$ via the embedding $u \mapsto (u, u^{-1})$ .

`diagonalUnits`

Under the same hypotheses, $\Delta_{p,K}$ is defined to be the monoid homomorphism

\Delta_{p,K} : \mathcal{O}_K^{\times} \longrightarrow \prod_{v \mid p} \mathcal{O}_{K_v}^{\times}

whose $v$ -th component is the map on unit groups induced by the canonical algebra homomorphism $\mathcal{O}_K \to \mathcal{O}_{K_v}$ ; that is, a global unit $u$ is sent to the family whose $v$ -th entry is the image of $u$ in $\mathcal{O}_{K_v}$ , regarded as a unit there. It is a homomorphism of multiplicative monoids (hence of groups) only; the definition asserts nothing about injectivity, continuity, or the nature of the image.

`unitClosure`

Under the same hypotheses, $\overline{E}_{p,K}$ is defined to be the following subgroup of $\mathrm{SemilocalUnits}(p,K) = \prod_{v\mid p}\mathcal{O}_{K_v}^{\times}$ . Write $E$ for the image subgroup $\Delta_{p,K}(\mathcal{O}_K^{\times})$ of global units under the diagonal map just described, and for a natural number $m$ write $U^{m}$ for the image subgroup of the $m$ -th power homomorphism $x \mapsto x^{m}$ on $U := \prod_{v\mid p}\mathcal{O}_{K_v}^{\times}$ , i.e. the subgroup of $m$ -th powers. Then

\overline{E}_{p,K} \;=\; \bigcap_{n \in \mathbb{N}} \Big( E \vee U^{p^{\,n+1}} \Big),

where $E \vee U^{p^{n+1}}$ denotes the join in the lattice of subgroups, i.e. the subgroup generated by $E$ and by all $p^{n+1}$ -st powers (since the ambient group is commutative this is the setwise product $E \cdot U^{p^{n+1}}$ ). The index $n$ ranges over all of $\mathbb{N}$ starting at $0$ , so the exponents occurring are $p^{1}, p^{2}, p^{3}, \dots$ and never $p^{0} = 1$ ; the intersection is over the complete lattice infimum, i.e. it is the intersection of the underlying sets. No topological notion of closure is used in the definition, and no closedness of the resulting subgroup is asserted.

`zpRankBelow`

This is a general-purpose definition, stated for an arbitrary type $G$ equipped with a commutative group structure and, independently, an arbitrary topology (no compatibility between the group operations and the topology is assumed — in particular no continuity of multiplication or inversion, and no separation axiom), together with a prime $p$ (from the ambient hypotheses, needed to speak of $\mathbb{Z}_p$ ), a natural number $\mathrm{bound}$ , and a subgroup $H \le G$ . Let $A_n$ denote the group $\mathbb{Z}_p^{\,n}$ of $n$ -tuples of $p$ -adic integers under pointwise addition, viewed as a multiplicative group by transport of structure (its topology is likewise transported from the product topology on $\mathbb{Z}_p^{\,n}$ ). Define

S \;=\; \Big\{ n \in \mathbb{N} \;:\; n \le \mathrm{bound} \ \text{ and } \ \exists\, f : A_n \to G \ \text{a monoid homomorphism with } f \text{ injective}, f \text{ continuous, and } f(x) \in H \text{ for every } x \in A_n \Big\}.

Then $\mathrm{zpRankBelow}_p(\mathrm{bound}, H)$ is defined to be $\sup S$ , computed as the supremum in $\mathbb{N}$ (which by convention returns $0$ when the set is empty or unbounded above — here the set is bounded above by $\mathrm{bound}$ by construction). The map $f$ is required only to be a homomorphism for the multiplicative structure: it need not be $\mathbb{Z}_p$ -linear, need not be a topological embedding, need not have closed or discrete image, and $H$ need not be closed. Note the degenerate member $n = 0$ : $A_0$ is the trivial group, the unique homomorphism out of it is injective and continuous and sends its only element to the identity of $G$ , which lies in $H$ ; hence $0 \in S$ always, $S$ is nonempty and bounded, and the supremum is an attained maximum. Thus the value is the largest $n \le \mathrm{bound}$ for which such an injective continuous multiplicative map $\mathbb{Z}_p^{\,n} \to G$ landing inside $H$ exists.

`defect`

Under the standing hypotheses ( $p$ prime, $K$ a number field), $\mathrm{defect}(p,K)$ is defined to be the natural number

\mathrm{defect}(p,K) \;=\; \mathrm{rank}(\mathcal{O}_K^{\times}) \;-\; \mathrm{zpRankBelow}_p\big([K:\mathbb{Q}],\; \overline{E}_{p,K}\big),

where: $\mathrm{rank}(\mathcal{O}_K^{\times})$ is Mathlib's unit rank of $K$ , defined as $\#\{\text{infinite places of } K\} - 1$ (i.e. $r_1 + r_2 - 1$ , itself a truncated natural-number subtraction); the bound supplied to $\mathrm{zpRankBelow}$ is $[K:\mathbb{Q}] = \dim_{\mathbb{Q}} K$ ; and the subgroup supplied is $\overline{E}_{p,K} = \bigcap_{n}\big(\Delta_{p,K}(\mathcal{O}_K^{\times}) \cdot U^{p^{n+1}}\big)$ inside $U = \prod_{v\mid p}\mathcal{O}_{K_v}^{\times}$ , as described above, with $U$ carrying the product-of-units-topologies mentioned above. The subtraction is truncated subtraction on $\mathbb{N}$ : if the second term exceeds the first, the value is $0$ rather than a negative number.

`LeopoldtConjecture`

Under the standing hypotheses ( $p$ a prime, $K$ a number field), $\mathrm{LeopoldtConjecture}(p,K)$ is defined to be the proposition

\mathrm{defect}(p,K) = 0,

that is, with all definitions unfolded, the proposition that

r_1 + r_2 - 1 \;=\; \max\Big\{\, n \le [K:\mathbb{Q}] \;:\; \exists\ \text{an injective continuous multiplicative homomorphism } \mathbb{Z}_p^{\,n} \to \textstyle\prod_{v\mid p}\mathcal{O}_{K_v}^{\times} \text{ whose image lies in } \bigcap_{m \ge 1}\big(\Delta_{p,K}(\mathcal{O}_K^{\times})\cdot \big(\textstyle\prod_{v\mid p}\mathcal{O}_{K_v}^{\times}\big)^{p^{m}}\big) \,\Big\}

holds after truncated subtraction — i.e., because the subtraction is truncated at $0$ , the proposition asserts only the inequality

\mathrm{rank}(\mathcal{O}_K^{\times}) \;\le\; \mathrm{zpRankBelow}_p\big([K:\mathbb{Q}], \overline{E}_{p,K}\big),

and is satisfied in particular whenever the right-hand quantity is at least the unit rank, including any case where it exceeds it. This is a definition of a proposition, not a theorem: nothing here is proved, and no claim is made that the proposition is true for any particular $p$ and $K$ .

Human review

Endorsed by Shuze Chen · Sep 9, 2026
Endorsed by kbuzzard · Sep 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The Leopoldt defect DL(K)\mathcal{D}_L(\mathbb{K})DL​(K) of a number field at ppp

PrimesOver

The finiteness instance for PrimesOver

SemilocalUnits

diagonalUnits

unitClosure

zpRankBelow

defect

LeopoldtConjecture