The torsion subgroup of a topologically finitely generated abelian pro-p group

The structure theorem identifies a topologically finitely generated abelian pro-p group A with ℤ_p ^ r × T for a finite abelian p-group T. This file describes the two factors of that decomposition and proves uniqueness of the rank and elementary divisors.

• The finite factor T is the torsion subgroup of A. Consequently the torsion subgroup is finite and closed, and it is open exactly when A is finite.
• The quotient A ⧸ torsion A is topologically isomorphic to ℤ_p ^ r; in particular a torsion-free topologically finitely generated abelian pro-p group is ℤ_p ^ r.
• The rank is unique: in any two decompositions A ≅ ℤ_p ^ r × T ≅ ℤ_p ^ r' × T' with T and T' torsion, r = r', because both ℤ_p ^ r and ℤ_p ^ r' are the quotient by the torsion subgroup and a continuous additive isomorphism ℤ_p ^ r ≃ ℤ_p ^ r' is ℤ_p-linear. The uniqueness of the torsion factor, T ≅ T', needs no pro-p hypothesis and is TauCeti.torsionFactorAddEquiv in TauCeti.GroupTheory.Torsion.
• When the finite factors are products of ZMod (p ^ e i) with positive exponents, that torsion-factor equivalence determines the exponents up to a bijection of the index types.
• For the canonical ℤ_[p]-module TauCeti.IsProP.module, the torsion submodule is the torsion subgroup, and the decomposition holds as topological ℤ_[p]-modules: the module is continuously linearly isomorphic to ℤ_p ^ r times its torsion submodule. This is the form of the structure theorem in which T is literally the torsion subgroup and the splitting respects the ℤ_[p]-action and the topology.

Finiteness of the torsion subgroup is what makes the torsion subgroup of the abelianisation of a topologically finitely generated pro-p group a finite invariant; the q-invariant of a Demushkin group is read off from it.

Main results

• TauCeti.IsProP.finite_torsion, TauCeti.IsProP.isClosed_torsion, TauCeti.IsProP.isOpen_torsion_iff_finite: the torsion subgroup is finite, closed, and open exactly when the group is finite.
• TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt: a torsion-free topologically finitely generated abelian pro-p group is topologically isomorphic to ℤ_p ^ r.
• TauCeti.IsProP.exists_continuousMulEquiv_quotient_torsion_pi_padicInt: the quotient by the torsion subgroup is topologically isomorphic to ℤ_p ^ r.
• TauCeti.eq_of_continuousMulEquiv_pi_padicInt_prod: uniqueness of the rank r.
• TauCeti.exists_equiv_exponents_of_continuousMulEquiv_pi_padicInt_prod_pi_zmod: uniqueness of the positive elementary-divisor exponents up to reindexing.
• TauCeti.IsProP.mem_torsion_module_iff, TauCeti.IsProP.finite_torsion_module: the torsion submodule of the canonical ℤ_[p]-module is the torsion subgroup, and is finite.
• TauCeti.IsProP.isTorsionFree_module_iff: the canonical ℤ_[p]-module is torsion-free exactly when the group is.
• TauCeti.IsProP.exists_continuousLinearEquiv_pi_padicInt_prod_torsion: the structure theorem as a continuous ℤ_[p]-linear equivalence A ≃ ℤ_p ^ r × T, with T the torsion submodule.

References

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

theorem TauCeti.eq_of_continuousMulEquiv_pi_padicInt_prod {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] {r r' : ℕ} {T : Type u_2} {T' : Type u_3} [AddCommGroup T] [TopologicalSpace T] [AddCommGroup T'] [TopologicalSpace T'] (hT : IsAddTorsion T) (hT' : IsAddTorsion T') (e : A ≃ₜ* Multiplicative ((Fin r → ℤ_[p]) × T)) (e' : A ≃ₜ* Multiplicative ((Fin r' → ℤ_[p]) × T')) : r = r'

Uniqueness of the rank in the structure theorem. Two decompositions of a topological abelian group as ℤ_p ^ r × T and ℤ_p ^ r' × T', with T and T' torsion, have r = r': both ℤ_p ^ r and ℤ_p ^ r' are the quotient by the torsion subgroup.

theorem TauCeti.exists_equiv_exponents_of_continuousMulEquiv_pi_padicInt_prod_pi_zmod {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] {r r' : ℕ} {ι : Type u_2} {κ : Type u_3} [Finite ι] [Finite κ] (e : ι → ℕ) (e' : κ → ℕ) (he : ∀ (i : ι), 0 < e i) (he' : ∀ (j : κ), 0 < e' j) (f : A ≃ₜ* Multiplicative ((Fin r → ℤ_[p]) × ((i : ι) → ZMod (p ^ e i)))) (f' : A ≃ₜ* Multiplicative ((Fin r' → ℤ_[p]) × ((j : κ) → ZMod (p ^ e' j)))) : ∃ (σ : ι ≃ κ), ∀ (i : ι), e i = e' (σ i)

Two decompositions into a finite power of ℤ_p and a finite product of nontrivial cyclic p-groups have the same elementary-divisor exponents up to reindexing. The decompositions themselves suffice; no compactness, finite-generation, or pro-p assumption on A is needed.

theorem TauCeti.IsProP.finite_torsion {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) : Finite ↥(CommGroup.torsion A)

The torsion subgroup of a topologically finitely generated abelian pro-p group is finite: it is the finite factor of the structure theorem.

theorem TauCeti.IsProP.isClosed_torsion {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) : IsClosed ↑(CommGroup.torsion A)

The torsion subgroup of a topologically finitely generated abelian pro-p group is closed.

theorem TauCeti.IsProP.isOpen_torsion_iff_finite {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) : IsOpen ↑(CommGroup.torsion A) ↔ Finite A

The torsion subgroup of a topologically finitely generated abelian pro-p group is open exactly when the group is finite, that is when the free rank of the structure theorem is 0.

theorem TauCeti.IsProP.exists_continuousMulEquiv_pi_padicInt {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] [IsMulTorsionFree A] (hA : IsProP p A) (hfg : IsTopologicallyFinitelyGenerated A) : ∃ (r : ℕ), Nonempty (A ≃ₜ* Multiplicative (Fin r → ℤ_[p]))

Structure theorem for torsion-free topologically finitely generated abelian pro-p groups. Such a group is topologically isomorphic to ℤ_p ^ r.

theorem TauCeti.IsProP.exists_continuousMulEquiv_quotient_torsion_pi_padicInt {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 : ℕ), Nonempty (A ⧸ CommGroup.torsion A ≃ₜ* Multiplicative (Fin r → ℤ_[p]))

The torsion-free quotient of a topologically finitely generated abelian pro-p group is ℤ_p ^ r. The quotient by the torsion subgroup is topologically isomorphic to the free factor of the structure theorem.

theorem TauCeti.IsProP.mem_torsion_module_iff {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (x : Additive A) : x ∈ Submodule.torsion ℤ_[p] (Additive A) ↔ Additive.toMul x ∈ CommGroup.torsion A

For the canonical ℤ_[p]-module TauCeti.IsProP.module of an abelian pro-p group, the torsion submodule is the torsion subgroup.

theorem TauCeti.IsProP.isTorsionFree_module_iff {p : ℕ} [Fact (Nat.Prime p)] {A : Type u_1} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) : Module.IsTorsionFree ℤ_[p] (Additive A) ↔ IsMulTorsionFree A

The canonical ℤ_[p]-module of an abelian pro-p group is torsion-free exactly when the group is.

theorem TauCeti.IsProP.finite_torsion_module {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) : Finite ↥(Submodule.torsion ℤ_[p] (Additive A))

The torsion submodule of the canonical ℤ_[p]-module of a topologically finitely generated abelian pro-p group is finite.

theorem TauCeti.IsProP.exists_continuousLinearEquiv_pi_padicInt_prod_torsion {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 : ℕ), Nonempty (Additive A ≃L[ℤ_[p]] (Fin r → ℤ_[p]) × ↥(Submodule.torsion ℤ_[p] (Additive A)))

Structure theorem for topologically finitely generated abelian pro-p groups, as topological ℤ_[p]-modules. The canonical ℤ_[p]-module TauCeti.IsProP.module of such a group is continuously linearly isomorphic to ℤ_p ^ r × T, where T is its torsion submodule, which is finite by TauCeti.IsProP.finite_torsion_module.