map_id — Mathlib

English

Sending the identity map on G yields the identity map on the abelianization: map (id_G) = id_{Abelianization G}.

Русский

Отображение id_G на абеллиановизацию равно тождественному отображению: map (id_G) = id_{Abelianization G}.

LaTeX

$$$$ \\mathrm{map}(\\mathrm{id}_G) = \\mathrm{id}_{\\mathrm{Abelianization}(G)}. $$$$

Lean4

@[simp]
theorem map_id : map (MonoidHom.id G) = MonoidHom.id (Abelianization G) :=
  hom_ext _ _ rfl

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