forget₂CommSemiRing_preservesLimitsOfSize

English

The forgetful functor forget₂ CommRingCat CommSemiRingCat preserves limits of size.

Русский

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

LaTeX

$$$\mathrm{forget}_2\text{CommRingCat PreservesLimitsOfSize}$$$

Lean4

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

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