English
There is a forgetful functor from CommRingCat to CommMonCat that sends a commutative ring to its underlying commutative monoid under multiplication, and sends a ring hom to the corresponding monoid hom.
Русский
Существует функтор забывания из CommRingCat в CommMonCat, отображающий коммутативное кольцо как коммутативный моноид умножения, а кольцевый гомоморфизм — в моноидный гомоморфизм.
LaTeX
$$$\text{forget₂ } CommRingCat CommMonCat$ sends $R$ to its multiplicative monoid $(R, \cdot, 1)$ and $f: R\to S$ to the monoid hom $f.hom$.$$
Lean4
/-- The forgetful functor from commutative rings to (multiplicative) commutative monoids. -/
instance hasForgetToCommMonCat : HasForget₂ CommSemiRingCat CommMonCat where
forget₂ :=
{ obj := fun R ↦ CommMonCat.of R
map := fun f ↦ CommMonCat.ofHom f.hom.toMonoidHom }
