hasForgetToAddCommMonCat — Mathlib

English

There is a forgetful functor from SemiRingCat to AddCommMonCat mapping objects to AddCommMonCat.of R and morphisms to the corresponding additive-moniod morphisms obtained from f.hom.

Русский

Существует забывающий функтор из SemiRingCat в AddCommMonCat, переводящий объекты в AddCommMonCat.of R и морфизмы в соответствующие моноид-морфизмы добавления, полученные из f.hom.

LaTeX

$$$ F(R) = \mathrm{AddCommMonCat.of}(R),\quad F(f) = \mathrm{AddCommMonCat.ofHom}(f.\mathrm{hom}).\mathrm{toAddMonoidHom}. $$$

Lean4

instance hasForgetToAddCommMonCat : HasForget₂ SemiRingCat AddCommMonCat where
  forget₂ :=
    { obj := fun R ↦ AddCommMonCat.of R
      map := fun f ↦ AddCommMonCat.ofHom f.hom.toAddMonoidHom }

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