# 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]
:

## Equations

- (_ : Subgroup.Normal (Subgroup.topologicalClosure (commutator G))) = (_ : Subgroup.Normal (Subgroup.topologicalClosure (commutator G)))

@[inline, reducible]

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

## Instances For

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

## Equations

- TopologicalAbelianization.commGroup G = let src := inferInstance; CommGroup.mk (_ : ∀ (x y : TopologicalAbelianization G), x * y = y * x)