English
The forgetful functor from groups to monoids preserves all limits of shape J (for small J). In particular, the underlying monoid of a limit is the limit in MonCat.
Русский
Функтор забывания из групп в моноиды сохраняет предельные конусы любой формы J для малых J; т. е. биследование ограничивается в MonCat.
LaTeX
$$$ \forall J\, [\text{Small}(J) \Rightarrow \mathrm{PreservesLimitsOfSize}(J, \text{forget }\mathrm{GrpCat} \mathrm{MonCat})] $$$
Lean4
/-- The forgetful functor from groups to monoids preserves all limits.
This means the underlying monoid of a limit can be computed as a limit in the category of monoids.
-/
@[to_additive (relevant_arg := 100) AddGrpCat.forget₂AddMonPreservesLimitsOfSize /--
The forgetful functor from additive groups to additive monoids preserves all limits.
This means the underlying additive monoid of a limit can be computed as a limit in the category of
additive monoids. -/
]
instance forget₂Mon_preservesLimitsOfSize [UnivLE.{v, u}] : PreservesLimitsOfSize.{w, v} (forget₂ GrpCat.{u} MonCat.{u})
where preservesLimitsOfShape {J _} := { }
