TopologicalAbelianization — Mathlib

English

The topological abelianization of a topological group G is the quotient of G by the topological closure of its commutator subgroup.

Русский

Топологическая абеллизация группы G есть факторгруппа G по топологическому замыканию коммутатора.

LaTeX

$$$\\mathrm{TopologicalAbelianization}(G) = G \\/\\; \\mathrm{Subgroup.topologicalClosure}(\\mathrm{commutator}(G))$$$

Lean4

/-- The topological abelianization of `absoluteGaloisGroup`, that is, the quotient of
  `absoluteGaloisGroup` by the topological closure of its commutator subgroup. -/
abbrev TopologicalAbelianization :=
  G ⧸ Subgroup.topologicalClosure (commutator G)

Похожие утверждения