Prove2Me

Functoriality of the bounded pp-adic subgroup rank

Proved
Leopoldt.zpRankBelow_le_of_continuous_injective

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

number-theoryp-adicunits

Let pp be prime, and let HH and H′H' be subgroups of commutative topological groups GG and G′G'. Suppose a continuous injective homomorphism f:G→G′f:G\to G' carries HH into H′H'. For bounds b≤b′b\le b', the bounded pp-adic ranks obey

rank⁡p,≤b(H)≤rank⁡p,≤b′(H′).\operatorname{rank}_{p,\le b}(H)\le\operatorname{rank}_{p,\le b'}(H').

Here the bounded rank is the largest nn within the stated bound for which a continuous injection of Zpn\mathbb Z_p^n into the ambient group lands in the subgroup. This result packages the functorial principle used when unit closures are transported along field embeddings and other injective maps.

Formalization Note The topology and group structure on the targets are supplied as assumptions; the homomorphism is explicitly required to be continuous and injective.

Preamble
import Definitions.Def_LeopoldtDefect
Formal statement
namespace Leopoldt
theorem zpRankBelow_le_of_continuous_injective (p : ℕ) [Fact p.Prime]
    {G G' : Type*} [CommGroup G] [TopologicalSpace G]
    [CommGroup G'] [TopologicalSpace G'] {b b' : ℕ}
    (f : G →* G') (hf : Function.Injective f) (hc : Continuous f)
    {H : Subgroup G} {H' : Subgroup G'}
    (hmap : ∀ g ∈ H, f g ∈ H') (hb : b ≤ b') :
    zpRankBelow p b H ≤ zpRankBelow p b' H' := by sorry
end Leopoldt
Source
Formal consequence of the rank definition in LeopoldtDefect, based on Preda Mihăilescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544v4, Section 1.1, p. 3 (p-adic closure and rank), and Section 1.3, Remark 1.A, p. 5 (behavior of defects under embeddings in finite extensions).

View graph