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] : Subgroup.Normal (Subgroup.topologicalClosure (commutator 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

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

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

Equations

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