The maximal pro-p quotient of the topological abelianization

Combining the universal properties of the topological abelianization and of the maximal pro-p quotient: a continuous homomorphism from a topological group G to a commutative profinite pro-p group factors through TopologicalAbelianization G and then through its maximal pro-p quotient G^ab(p). Hence it kills every element of G whose class in G^ab(p) is trivial.

Main results

• TauCeti.eq_one_of_maximalProPQuotient_mk_eq_one: every continuous homomorphism to a commutative pro-p group kills the elements that die in the maximal pro-p abelian quotient.

theorem TauCeti.eq_one_of_maximalProPQuotient_mk_eq_one {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A] [T1Space A] [CompactSpace A] [TotallyDisconnectedSpace A] (hA : IsProP p A) (f : G →ₜ* A) {g : G} (hg : (maximalProPQuotient.mk p (TopologicalAbelianization G)) ↑g = 1) : f g = 1

Every continuous homomorphism from G to a commutative pro-p group kills the elements that die in the maximal pro-p quotient of the topological abelianization of G.