absoluteGaloisGroupAbelianization

English

The topological abelianization is the quotient of the absolute Galois group by the closure of its commutator subgroup.

Русский

Топологическая абеллианизация — это факторгруппа абсолютной Галуа-группы по замыканию её группы коммутаторов.

LaTeX

$$$$\mathrm{absoluteGaloisGroupAbelianization}(K) = \mathrm{TopologicalAbelianization}(\mathrm{Field.absoluteGaloisGroup}\,K)$$$$

Lean4

/-- The topological abelianization of `absoluteGaloisGroup`, that is, the quotient of
  `absoluteGaloisGroup` by the topological closure of its commutator subgroup. -/
abbrev absoluteGaloisGroupAbelianization :=
  TopologicalAbelianization (G_K K)

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