forget₂_grp_map_ofHom — Mathlib

English

The forgetful functor from CommGrpCat to GrpCat sends ofHom f to GrpCat.ofHom f for any f: X →* Y.

Русский

Забывающий функтор от CommGrpCat к GrpCat отправляет ofHom f в GrpCat.ofHom f для любого f: X →* Y.

LaTeX

$$$$ \forall X,Y\,[\mathrm{CommGroup}(X)], [\mathrm{CommGroup}(Y)],\ (f : X \to_* Y),\ (forget_{CommGrpCat,GrpCat}).map(CommGrpCat.ofHom f) = GrpCat.ofHom f. $$$$

Lean4

@[to_additive (attr := simp)]
theorem forget₂_grp_map_ofHom {X Y : Type u} [CommGroup X] [CommGroup Y] (f : X →* Y) :
    (forget₂ CommGrpCat GrpCat).map (ofHom f) = GrpCat.ofHom f :=
  rfl

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