The topological abelianization of a group.

This file defines the topological abelianization of a topological group.

Main definitions

• TopologicalAbelianization: defines the topological abelianization of a group G as the quotient of G by the topological closure of its commutator subgroup..

Main results

• instNormalCommutatorClosure : the topological closure of the commutator of a topological group G is a normal subgroup.

Tags

group, topological abelianization

instance instNormalCommutatorClosure (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] : (commutator G).topologicalClosure.Normal

@[reducible, inline]

abbrev TopologicalAbelianization (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] : Type u_1

The topological abelianization of absoluteGaloisGroup, that is, the quotient of absoluteGaloisGroup by the topological closure of its commutator subgroup.

Equations

• TopologicalAbelianization G = (G ⧸ (commutator G).topologicalClosure)

instance TopologicalAbelianization.commGroup (G : Type u_1) [Group G] [TopologicalSpace G] [TopologicalGroup G] : CommGroup (TopologicalAbelianization G)

Equations

• TopologicalAbelianization.commGroup G = CommGroup.mk ⋯