forget₂SemiRing_preservesLimitsOfSize

English

The forgetful functor from rings to types preserves all limits.

Русский

Функтор забывания из колец в множества сохраняет все пределы.

LaTeX

$$$\mathrm{forget}\!:\mathrm{RingCat} \to \mathrm{Type}$ preserves limits.$$

Lean4

/-- The forgetful functor from rings to semirings preserves all limits.
-/
instance forget₂SemiRing_preservesLimitsOfSize [UnivLE.{v, u}] :
    PreservesLimitsOfSize.{w, v} (forget₂ RingCat SemiRingCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F)
          (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _) }

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