English
If J is u-small, the forgetful functor from CommGrpCat to CommMonCat preserves limits of shape J.
Русский
Если J малоразмерен по унивору u, функтор забывания из CommGrpCat в CommMonCat сохраняет пределы формы J.
LaTeX
$$$[Small\\;J]\\;\\PreservesLimitsOfShape\\;(forget_{CommGrpCat\\to CommMonCat})$$$
Lean4
/-- If `J` is `u`-small, the forgetful functor from `CommGrpCat.{u}` to `CommMonCat.{u}`
preserves limits of shape `J`. -/
@[to_additive AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfShape /--
If `J` is `u`-small, the forgetful functor from `AddCommGrpCat.{u}`
to `AddCommMonCat.{u}` preserves limits of shape `J`. -/
]
instance forget₂CommMon_preservesLimitsOfShape [Small.{u} J] :
PreservesLimitsOfShape J (forget₂ CommGrpCat.{u} CommMonCat.{u}) where
preservesLimit
{F} :=
preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F) (forget₂CommMon_preservesLimitsAux.{v, u} F)
