English
The forgetful functor from commutative groups to commutative monoids preserves all limits.
Русский
Функтор забывания из коммутативных групп в коммутативные моноиды сохраняет все пределы.
LaTeX
$$$\\operatorname{PreservesLimits}(\\mathrm{forget}_{CommGrpCat\\to CommMonCat})$$$
Lean4
/-- The forgetful functor from commutative groups to commutative monoids preserves all limits.
(That is, the underlying commutative monoids could have been computed instead as limits
in the category of commutative monoids.)
-/
@[to_additive AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize /--
The forgetful functor from additive commutative groups to additive commutative monoids
preserves all limits. (That is, the underlying additive commutative monoids could have been
computed instead as limits in the category of additive commutative monoids.) -/
]
instance forget₂CommMon_preservesLimitsOfSize [UnivLE.{v, u}] :
PreservesLimitsOfSize.{w, v} (forget₂ CommGrpCat CommMonCat.{u}) where preservesLimitsOfShape := { }
