The degree-zero graded piece and topological abelianization

The degree-zero piece of the closed lower central series is the quotient by the closure of the commutator subgroup. This file identifies it, as a topological additive group, with Mathlib's topological abelianization. The equivalence sends the class of an element to its abelianization class, so computations in the first graded piece can use the usual quotient API.

noncomputable def TauCeti.lcsGradedPieceZeroEquiv {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : gradedPiece 0 G 0 ≃ₜ+ Additive (TopologicalAbelianization G)

The zero-th graded piece of the closed lower central series, with its quotient topology, is the topological abelianization of G in additive notation.

@[simp]

theorem TauCeti.lcsGradedPieceZeroEquiv_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : lcsGradedPieceZeroEquiv (gradedMkZero 0 G g) = Additive.ofMul ↑g

The degree-zero equivalence sends the class of g to the class of g in the topological abelianization.

@[simp]

theorem TauCeti.lcsGradedPieceZeroEquiv_symm_mk {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (g : G) : lcsGradedPieceZeroEquiv.symm (Additive.ofMul ↑g) = gradedMkZero 0 G g

The inverse equivalence sends an abelianization class to its degree-zero graded class.