The structure theorem for topologically finitely generated abelian pro-p groups

A topologically finitely generated abelian pro-p group A is topologically isomorphic to ℤ_p ^ r × T, where T = ∏ i : Fin m, ℤ/p^(e i) is a finite abelian p-group carrying the discrete topology and every exponent e i is positive, so that the finite factor has no trivial summand. The isomorphism is an isomorphism of topological groups. This is the abelian case of the classification of finitely generated pro-p groups; it describes, for instance, the abelianisation of any topologically finitely generated pro-p group.

The statement records a topological group isomorphism. Every continuous homomorphism between abelian pro-p groups commutes with p-adic exponentiation, TauCeti.IsProP.map_padicPow, so no information is lost; the decomposition as topological modules for the canonical p-adic exponentiation TauCeti.IsProP.module, with the torsion submodule as finite factor, is TauCeti.IsProP.exists_continuousLinearEquiv_pi_padicInt_prod_torsion. The rank r and the exponents e i, up to reindexing, are invariants of A. The identification of T with the torsion subgroup and the uniqueness results are proved in TauCeti.Topology.Algebra.Group.Profinite.ProP.Torsion. In particular, TauCeti.exists_equiv_exponents_of_continuousMulEquiv_pi_padicInt_prod_pi_zmod compares the exponents in any two decompositions with positive exponents; its algebraic input is ZMod.exists_equiv_exponents_of_pi_pow_addEquiv.

Main result

• TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt_prod_pi_zmod: a topologically finitely generated abelian pro-p group is topologically isomorphic to ℤ_p ^ r × ∏ i : Fin m, ℤ/p^(e i).

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 4.3.

theorem TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt_prod_pi_zmod {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (hfg : IsTopologicallyFinitelyGenerated A) : ∃ (r : ℕ) (m : ℕ) (e : Fin m → ℕ), (∀ (i : Fin m), 0 < e i) ∧ Nonempty (A ≃ₜ* Multiplicative ((Fin r → ℤ_[p]) × ((i : Fin m) → ZMod (p ^ e i))))

Structure theorem for topologically finitely generated abelian pro-p groups. Such a group is topologically isomorphic to ℤ_p ^ r × ∏ i : Fin m, ℤ/p^(e i) with every e i positive, where the finite factor carries the discrete topology.