The universal property of the topological abelianization

The topological abelianization G ⧸ closure [G, G] of a topological group G is the universal continuous homomorphism from G to a commutative T1 topological group: such a homomorphism kills every commutator, so its closed kernel contains the closure of the commutator subgroup, and it factors uniquely through the quotient. This is the topological counterpart of Abelianization.lift; it is what identifies the abelianization of a concrete profinite group with an abelian profinite group given by its universal property.

Main definitions

• TopologicalAbelianization.lift: the continuous homomorphism TopologicalAbelianization G →ₜ* A induced by a continuous homomorphism G →ₜ* A into a commutative T1 group.

Main results

• TopologicalAbelianization.topologicalClosure_commutator_le_ker: the closure of the commutator subgroup lies in the kernel of every continuous homomorphism to a commutative T1 group.
• TopologicalAbelianization.lift_mk, TopologicalAbelianization.lift_unique: the factorisation and its uniqueness.
• TopologicalAbelianization.hom_ext: a continuous homomorphism out of the topological abelianization is determined by its values on the classes of elements of G.

theorem TopologicalAbelianization.topologicalClosure_commutator_le_ker {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [T1Space A] (f : G →ₜ* A) : (commutator G).topologicalClosure ≤ (↑f).ker

The closure of the commutator subgroup lies in the kernel of every continuous homomorphism to a commutative T1 group: the kernel is closed and contains all commutators.

noncomputable def TopologicalAbelianization.lift {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [T1Space A] (f : G →ₜ* A) : TopologicalAbelianization G →ₜ* A

The universal property of the topological abelianization. A continuous homomorphism from G to a commutative T1 group factors through TopologicalAbelianization G.

Equations

• TopologicalAbelianization.lift f = TauCeti.ContinuousMonoidHom.quotientLift (commutator G).topologicalClosure f ⋯

@[simp]

theorem TopologicalAbelianization.lift_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [T1Space A] (f : G →ₜ* A) (x : G) : (lift f) ↑x = f x

The lift of f evaluates as f on the class of an element.

@[simp]

theorem TopologicalAbelianization.lift_comp_quotientMk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [T1Space A] (f : G →ₜ* A) : (lift f).comp (TauCeti.ContinuousMonoidHom.quotientMk (commutator G).topologicalClosure) = f

The lift of f composed with the projection is f.

theorem TopologicalAbelianization.lift_unique {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {A : Type u_2} [CommGroup A] [TopologicalSpace A] [T1Space A] (f : G →ₜ* A) (g : TopologicalAbelianization G →ₜ* A) (hg : ∀ (x : G), g ↑x = f x) : g = lift f

A continuous homomorphism out of the topological abelianization that agrees with f on classes is the lift of f.

theorem TopologicalAbelianization.hom_ext {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {B : Type u_2} [Monoid B] [TopologicalSpace B] {g g' : TopologicalAbelianization G →ₜ* B} (h : ∀ (x : G), g ↑x = g' ↑x) : g = g'

Two continuous homomorphisms out of the topological abelianization that agree on the classes of elements of G are equal.

theorem TopologicalAbelianization.hom_ext_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {B : Type u_2} [Monoid B] [TopologicalSpace B] {g g' : TopologicalAbelianization G →ₜ* B} : g = g' ↔ ∀ (x : G), g ↑x = g' ↑x