lift_of — Mathlib

English

The lift of the canonical projection of G is the identity on the abelianization: lift of = id_{Abelianization G}.

Русский

Поднятие канонической проекции равно тождественному отображению на абеллиановизацию: lift of = id_{Abelianization G}.

LaTeX

$$$$ \\mathrm{lift}(\\mathrm{of}) = \\mathrm{id}_{\\mathrm{Abelianization}(G)}. $$$$

Lean4

@[simp]
theorem lift_of : lift of = MonoidHom.id (Abelianization G) :=
  lift.apply_symm_apply <| MonoidHom.id _

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