forget_preservesLimitsOfSize — Mathlib

English

The forgetful functor forget CommSemiRingCat preserves all limits.

Русский

Забывающий функтор forget CommSemiRingCat сохраняет все пределы.

LaTeX

$$$ \\mathrm{forget_preservesLimits} : \\text{PreservesLimits}( \\mathrm{forget CommSemiRingCat} )$$$

Lean4

/-- The forgetful functor from rings to types preserves all limits. (That is, the underlying
types could have been computed instead as limits in the category of types.)
-/
instance forget_preservesLimitsOfSize [UnivLE.{v, u}] : PreservesLimitsOfSize.{w, v} (forget CommSemiRingCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F) (Types.Small.limitConeIsLimit.{v, u} _) }

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