hasForgetToMonCat — Mathlib

English

There is a forgetful functor from the category of groups GrpCat to MonCat, sending a group to its underlying monoid and a group hom to the corresponding monoid hom.

Русский

Существует забывающий функтор из категории групп GrpCat в MonCat, отправляющий группу в ее лежащий в основе моноид и гомоморфизм группы — в соответствующий гомоморфизм моноидов.

LaTeX

$$$\\exists F:\\mathrm{GrpCat} \\to \\mathrm{MonCat}\\;\\big(F(\\mathrm{obj}\\,G)=\\mathrm{MonCat.of}G \\land\\forall f, F(f)=\\mathrm{MonCat.ofHom}(f.hom)\\big)$$$

Lean4

@[to_additive hasForgetToAddMonCat]
instance hasForgetToMonCat : HasForget₂ GrpCat MonCat
    where
  forget₂.obj X := MonCat.of X
  forget₂.map f := MonCat.ofHom f.hom

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