forget_preservesLimitsOfSize — Mathlib

English

The forgetful functor from RingCat to AddCommGroupCat preserves all limits.

Русский

Функтор забывания RingCat → AddCommGrpCat сохраняет все пределы.

LaTeX

$$$\text{forget}_2\text{AddCommGroup_preservesLimits} : \text{PreservesLimits}(\mathrm{forget}_2\,\text{RingCat}, \text{AddCommGrpCat})$$$

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.{v, v} (forget RingCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F) (Types.Small.limitConeIsLimit.{v, u} _) }

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