Rank of the $p$ -adic closure of $\varphi(\bar{E}(\mathbb{F}))\cdot\langle h_1,\dots,h_m\rangle$ is at most $\mathbb{Z}_p\text{-rk}\,\bar{E}(\mathbb{F}) + m$

Proved

Leopoldt.exists_continuous_injective_unitClosure_of_mem_iInf

by WCoram · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

iwasawa-theorynumber-theoryp-adicunits

Let $p$ be a prime and $\mathbb{F}$ , $\mathbb{K}$ number fields, with semilocal units $U_p(\mathbb{F})$ , $U_p(\mathbb{K})$ at $p$ and $p$ -adic closure of the global units $\bar{E}(\mathbb{F}) = \bigcap_{k > 0} \iota(E(\mathbb{F}))\,U_p(\mathbb{F})^{p^k} \subseteq U_p(\mathbb{F})$ , as in Section 1.1 of the source. Let $\varphi : U_p(\mathbb{F}) \to U_p(\mathbb{K})$ be any continuous injective group homomorphism, let $h_1, \dots, h_m \in U_p(\mathbb{K})$ , and consider the $p$ -adic closure

C \;=\; \bigcap_{k > 0} \varphi\bigl(\bar{E}(\mathbb{F})\bigr)\cdot\langle h_1, \dots, h_m\rangle\cdot U_p(\mathbb{K})^{p^k} \;\subseteq\; U_p(\mathbb{K}),

formed exactly as $\bar{E}$ is formed in the source. Suppose $f : \mathbb{Z}_p^{\,n} \to U_p(\mathbb{K})$ is a continuous injective homomorphism with values in $C$ . Then there are an integer $n'$ with

n \;\le\; n' + m

and a continuous injective homomorphism $f' : \mathbb{Z}_p^{\,n'} \to U_p(\mathbb{F})$ with values in $\bar{E}(\mathbb{F})$ .

In the language of ranks: the $\mathbb{Z}_p$ -rank of the $p$ -adic closure of $\varphi(\bar{E}(\mathbb{F}))\cdot\langle h_1,\dots,h_m\rangle$ is at most $\mathbb{Z}_p\text{-rk}\,\bar{E}(\mathbb{F}) + m$ . This is the statement that "the linear relations between $\mathbb{Z}$ -generators of the units of $E(\mathbb{K}_1)$ , which arise upon $p$ -adic completion, will be preserved under the embedding into the units $E(\mathbb{K})$ " of Remark 1.A: adjoining $m$ elements to a closed subgroup raises the $\mathbb{Z}_p$ -rank of the closure by at most $m$ , and the subgroup $\varphi(\bar{E}(\mathbb{F}))$ , being the image of a compact group under a continuous injection, has the same rank as $\bar{E}(\mathbb{F})$ . Applied with $\varphi$ the functorial map of Leopoldt.exists_semilocalHom and $h_i = \iota(g_i)$ the images of finitely many units of $\mathbb{K}$ that, together with $E(\mathbb{F})$ , generate a finite-index subgroup of $E(\mathbb{K})$ , it gives the topological half of Remark 1.A.

Formalization Note $\mathbb{Z}_p^{\,n}$ is Multiplicative (Fin n → ℤ_[p]); the closure $C$ is the infimum over $k$ of the subgroup joins (unitClosure p F).map φ ⊔ closure (range h) ⊔ range (powMonoidHom (p ^ (k + 1))), matching the shape of unitClosure in the definition file, so that $U_p^{p^k}$ is the range of the $p^k$ -th power map. The map $\varphi$ is an arbitrary continuous injective homomorphism, not necessarily the one induced by an inclusion $\mathbb{F} \subseteq \mathbb{K}$ ; no Algebra F K instance is assumed. The witness $n'$ is not required to satisfy $n' \le [\mathbb{F} : \mathbb{Q}]$ ; that bound is the separate statement Leopoldt.le_finrank_of_continuous_injective_semilocalUnits.

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem exists_continuous_injective_unitClosure_of_mem_iInf (p : ℕ) [Fact p.Prime]
    (F K : Type*) [Field F] [NumberField F] [Field K] [NumberField K]
    (φ : SemilocalUnits p F →* SemilocalUnits p K) (hφc : Continuous φ)
    (hφi : Function.Injective φ) {m : ℕ} (h : Fin m → SemilocalUnits p K) {n : ℕ}
    (f : Multiplicative (Fin n → ℤ_[p]) →* SemilocalUnits p K)
    (hf : Function.Injective f) (hc : Continuous f)
    (hmem : ∀ x, f x ∈ ⨅ k : ℕ, ((unitClosure p F).map φ ⊔ Subgroup.closure (Set.range h) ⊔
      (powMonoidHom (p ^ (k + 1))).range)) :
    ∃ (n' : ℕ) (f' : Multiplicative (Fin n' → ℤ_[p]) →* SemilocalUnits p F),
      n ≤ n' + m ∧ Function.Injective f' ∧ Continuous f' ∧ ∀ x, f' x ∈ unitClosure p F := by sorry
end Leopoldt

Source

Preda Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, https://arxiv.org/abs/1105.4544 (v4, 17 Feb 2016), Section 1.3 (Plan of the proof), Remark 1 part A, p. 5: "It follows from the fact that the linear relations between Z-generators of the units of E(K_1), which arise upon p-adic completion, will be preserved under the embedding into the units E(K)." This is that preservation statement, in the notation of Section 1.1, p. 3 (U, iota, Ebar = intersection over n of iota(E) U^{p^n}, Z_p-rank): adjoining m elements to phi(Ebar(K_1)) inside U(K) raises the Z_p-rank of the p-adic closure by at most m. Cited original for Remark 1.A: M. Laurent, Rang p-adique d'unites et action de groupes, J. reine angew. Math. 399 (1989), 81-108, introduction.

View graph

Rank of the ppp-adic closure of φ(Eˉ(F))⋅⟨h1,…,hm⟩\varphi(\bar{E}(\mathbb{F}))\cdot\langle h_1,\dots,h_m\rangleφ(Eˉ(F))⋅⟨h1​,…,hm​⟩ is at most Zp-rk Eˉ(F)+m\mathbb{Z}_p\text{-rk}\,\bar{E}(\mathbb{F}) + mZp​-rkEˉ(F)+m

Rank of the $p$ -adic closure of $\varphi(\bar{E}(\mathbb{F}))\cdot\langle h_1,\dots,h_m\rangle$ is at most $\mathbb{Z}_p\text{-rk}\,\bar{E}(\mathbb{F}) + m$