hasForgetToCommMonCat — Mathlib

English

For a commutative group hom f: X →* Y, the forgetful functor to CommMonCat sends ofHom f to CommMonCat.ofHom f.

Русский

Для гомоморфизма f: X →* Y между коммутативными группами забывающий функтор к CommMonCat отправляет ofHom f в CommMonCat.ofHom f.

LaTeX

$$$$ \forall X,Y\,[\mathrm{CommGroup}(X)], [\mathrm{CommGroup}(Y)] (f : X \to_* Y),\ (\text{forget}_{CommGrpCat,CommMonCat}).map(CommGrpCat.ofHom f) = CommMonCat.ofHom f. $$$$

Lean4

@[to_additive hasForgetToAddCommMonCat]
instance hasForgetToCommMonCat : HasForget₂ CommGrpCat CommMonCat
    where
  forget₂.obj X := CommMonCat.of X
  forget₂.map f := CommMonCat.ofHom f.hom

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