The bounded $\mathbb{Z}_p$ -rank is monotone in the subgroup

Proved

Leopoldt.zpRankBelow_mono_subgroup

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

leopoldtnumber-theory

Let $p$ be a prime and $G$ a commutative topological group. For a subgroup $H \le G$ and a bound $b \in \mathbb{N}$ , let $\operatorname{rk}_b(H)$ denote the largest $n \le b$ such that there is a continuous injective homomorphism $\mathbb{Z}_p^{\,n} \to G$ with image inside $H$ (this is zpRankBelow p b H from the mission definition file).

If $H \le H'$ are subgroups of $G$ , then

\operatorname{rk}_b(H) \le \operatorname{rk}_b(H').

Indeed every embedding of $\mathbb{Z}_p^{\,n}$ landing in $H$ also lands in $H'$ .

Preamble

import Definitions.Def_LeopoldtDefect

open NumberField

Formal statement

namespace Leopoldt
theorem zpRankBelow_mono_subgroup (p : ℕ) [Fact p.Prime] {G : Type*} [CommGroup G]
    [TopologicalSpace G] (b : ℕ) {H H' : Subgroup G} (h : H ≤ H') :
    zpRankBelow p b H ≤ zpRankBelow p b H' := by sorry
end Leopoldt

Source

Mission definition file Def_LeopoldtDefect (definition of zpRankBelow), after P. Mihailescu, On CM Z_p-extensions and the Leopoldt conjecture for CM fields, arXiv:1105.4544, Section 1.1 (Notations and fundamental facts)

View graph

The bounded Zp\mathbb{Z}_pZp​-rank is monotone in the subgroup

The bounded $\mathbb{Z}_p$ -rank is monotone in the subgroup