Prove2Me

Bounded pp-adic rank is invariant under finite-index subgroup passage

Proved
Leopoldt.zpRankBelow_eq_of_finite_relIndex

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

number-theoryp-adicunits

Let H′⊆HH'\subseteq H be subgroups of a commutative topological group, and suppose the quotient H/H′H/H' is finite. Then their bounded pp-adic ranks are equal for every bound bb:

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

The assertion is useful when replacing a subgroup of the semilocal units by a finite-index subgroup, such as one generated by suitable powers. It preserves the free Zp\mathbb Z_p-rank used to define the Leopoldt defect.

Formalization Note The finite-index condition is relative to HH, not the ambient group; the latter can have a much larger rank.

Preamble
import Definitions.Def_LeopoldtDefect
Formal statement
namespace Leopoldt
theorem zpRankBelow_eq_of_finite_relIndex (p : ℕ) [Fact p.Prime]
    {G : Type*} [CommGroup G] [TopologicalSpace G]
    (b : ℕ) {H H' : Subgroup G} (hsub : H' ≤ H)
    [H'.IsFiniteRelIndex H] :
    zpRankBelow p b H' = zpRankBelow p b H := by sorry
end Leopoldt
Source
Formal consequence of the bounded p-adic rank definition in Definitions.Def_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 (the p-adic rank of unit closures), and Section 1.3, Remark 1.A, p. 5 (finite-extension behavior). The finite-index power argument uses Mathlib.GroupTheory.Index, Subgroup.pow_mem_of_relIndex_ne_zero_of_dvd.

View graph