forget_preservesLimitsOfShape — Mathlib

English

The universe lift functor preserves limits of shape J.

Русский

Функтор подъёма вселенной сохраняет пределы формы J.

LaTeX

$$$\\text{uliftFunctorPreservesLimitsOfShape}(J)$$$

Lean4

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

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