forget_preservesLimitsOfShape — Mathlib

English

For every J, if J is small, the forgetful functor forget GrpCat preserves limits of shape J.

Русский

Для каждого малого J забывающий функтор забывания GrpCat сохраняет пределы формы J.

LaTeX

$$$ \forall J\, [\Small(J) \Rightarrow \mathrm{PreservesLimitsOfShape}(J, \mathrm{forget GrpCat})] $$$

Lean4

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

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