Functoriality of the semilocal units $U_p$ along an extension of number fields

Proved

Leopoldt.exists_semilocalHom

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

local-fieldsnumber-theoryp-adicunits

Let $p$ be a prime and let $\mathbb{F} \subseteq \mathbb{K}$ be number fields. For a number field $\mathbb{L}$ write $U_p(\mathbb{L}) = \prod_{\wp \mid p} \mathcal{O}_\wp^\times$ for the semilocal units at $p$ and $\iota_{\mathbb{L}} : E(\mathbb{L}) = \mathcal{O}(\mathbb{L})^\times \to U_p(\mathbb{L})$ for the diagonal embedding of the global units, as in Section 1.1 of the source.

Then there is a continuous injective group homomorphism

\varphi : U_p(\mathbb{F}) \longrightarrow U_p(\mathbb{K})

compatible with the diagonal embeddings: for every global unit $\varepsilon \in E(\mathbb{F})$ ,

\varphi\bigl(\iota_{\mathbb{F}}(\varepsilon)\bigr) = \iota_{\mathbb{K}}(\varepsilon),

where on the right $\varepsilon$ is regarded as a unit of $\mathcal{O}(\mathbb{K})$ through the inclusion $\mathcal{O}(\mathbb{F}) \subseteq \mathcal{O}(\mathbb{K})$ .

The map is assembled from the local ones: every prime $\mathfrak{P} \mid p$ of $\mathbb{K}$ lies over a unique prime $\wp \mid p$ of $\mathbb{F}$ , the completion $\mathbb{F}_\wp$ embeds continuously into $\mathbb{K}_\mathfrak{P}$ carrying local units to local units, and since every $\wp$ has at least one $\mathfrak{P}$ above it the resulting map on products is injective. This is the "embedding into the units $E(\mathbb{K})$ " that Remark 1.A of the source appeals to, packaged as a statement about the semilocal units so that it can be reused: it is the input for comparing the $p$ -adic closures $\bar{E}(\mathbb{F})$ and $\bar{E}(\mathbb{K})$ , and it is the construction behind the proved lemma Leopoldt.zpRankBelow_unitClosure_mono.

Formalization Note The fields are related by an Algebra F K instance, as in the milestone statement; no finiteness of $\mathbb{K}/\mathbb{F}$ is required, since number fields are finite over $\mathbb{Q}$ . SemilocalUnits p L is the product over the primes above $p$ of the unit groups of the completed rings of integers, with the product topology, and diagonalUnits p L is the diagonal embedding, both from the definition file. The unit of $\mathcal{O}(\mathbb{K})$ attached to $\varepsilon$ is Units.map of the ring map $\mathcal{O}(\mathbb{F}) \to \mathcal{O}(\mathbb{K})$ .

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem exists_semilocalHom (p : ℕ) [Fact p.Prime]
    (F K : Type*) [Field F] [NumberField F] [Field K] [NumberField K] [Algebra F K] :
    ∃ φ : SemilocalUnits p F →* SemilocalUnits p K, Continuous φ ∧ Function.Injective φ ∧
      ∀ ε : (𝓞 F)ˣ, φ (diagonalUnits p F ε) =
        diagonalUnits p K (Units.map (algebraMap (𝓞 F) (𝓞 K)).toMonoidHom ε) := 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.1 (Notations and fundamental facts), p. 3, where U = prod_{wp | p} O_wp^x and the diagonal embedding iota : E -> U are defined; and Section 1.3, Remark 1 part A, p. 5: "the linear relations ... will be preserved under the embedding into the units E(K)" - this statement packages that embedding at the level of semilocal units. The construction is the one carried out inside the accepted proof of Leopoldt.zpRankBelow_unitClosure_mono (uniformContinuous_algebraMap_liesOver and valuation_liesOver from Mathlib/NumberTheory/RamificationInertia/Valuation.lean).

View graph

Functoriality of the semilocal units UpU_pUp​ along an extension of number fields

Functoriality of the semilocal units $U_p$ along an extension of number fields