English
There is a forgetful functor from SemiRingCat to MonCat sending a semiring to its multiplicative monoid, and a semiring hom to the corresponding monoid hom derived from its additive-preserving hom.
Русский
Существует забывающий функтор из SemiRingCat в MonCat, отправляющий полукольцо в его умножающую моноидную структуру, а полукольцевый морфизм в соответствующий моидоморфизм, полученный из его гомоморфизма, сохраняющего сложение.
LaTeX
$$$ F :\mathrm{SemiRingCat} \to \mathrm{MonCat},\quad F(R) = \mathrm{MonCat.of}(R),\quad F(f) = \mathrm{MonCat.ofHom}(f.\mathrm{hom}).\mathrm{toMonoidHom}. $$$
Lean4
instance hasForgetToMonCat : HasForget₂ SemiRingCat MonCat where
forget₂ :=
{ obj := fun R ↦ MonCat.of R
map := fun f ↦ MonCat.ofHom f.hom.toMonoidHom }
