English
For a chosen universe size, the forgetful functor from CommGrpCat to CommMonCat preserves limits of that shape.
Русский
Для заданного размера вселенной функтор забывания сохраняет пределы заданной формы.
LaTeX
$$$\\PreservesLimitsOfShape J(\\mathrm{forget}_{CommGrpCat\\to CommMonCat})$$$
Lean4
/-- The forgetful functor from commutative groups to types preserves all limits. (That is, the
underlying types could have been computed instead as limits in the category of types.)
-/
@[to_additive /-- The forgetful functor from additive commutative groups to types preserves all limits.
(That is, the underlying types could have been computed instead as limits in the category of
types.) -/
]
instance forget_preservesLimitsOfSize : PreservesLimitsOfSize.{w, v} (forget CommGrpCat.{u}) :=
inferInstance
