forget_preservesLimitsOfShape — Mathlib

English

The forgetful functor forget MonCat to Types preserves limits of shape J (i.e., preserves the limit cones of shape J).

Русский

Забывающая функция forget MonCat → Types сохраняет пределы формы J (то есть сохраняет предел-конусы формы J).

LaTeX

$$$\text{PreservesLimitsOfShape } J\bigl(\text{forget MonCat}\bigr)$$$

Lean4

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

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