forget_preservesLimitsOfShape — Mathlib

English

If J is u-small, the forgetful functor forget CommMonCat.{u} → MonCat.{u} preserves limits of shape J.

Русский

Если J является u-малой, забывающий функтор forget CommMonCat.{u} → MonCat.{u} сохраняет пределы формы J.

LaTeX

$$$[\text{Small}.{u} J] \Rightarrow \operatorname{PreservesLimitsOfShape} J (\text{forget}\ \text{CommMonCat})$$$

Lean4

/-- If `J` is `u`-small, the forgetful functor from `CommMonCat.{u}` preserves limits of
shape `J`. -/
@[to_additive /-- If `J` is `u`-small, the forgetful functor from `AddCommMonCat.{u}`
    preserves limits of shape `J`. -/
    ]
instance forget_preservesLimitsOfShape [Small.{u} J] : PreservesLimitsOfShape J (forget CommMonCat.{u}) where
  preservesLimit
    {F} := preservesLimit_of_preserves_limit_cone (limitConeIsLimit F) (Types.Small.limitConeIsLimit (F ⋙ forget _))

Похожие утверждения