forget₂AddCommMon_preservesLimitsOfSize

English

Let F: J → SemiRingCat be a diagram. The forgetful functor from semirings to additive commutative monoids preserves all limits.

Русский

Пусть F: J → SemiRingCat задаёт диаграмму. Забывающий функтор из полупринождений в аддитивные коммутативные моноиды сохраняет все пределы.

LaTeX

$$$\operatorname{PreservesLimits}\big(\operatorname{forget}_2\, SemiRingCat\, AddCommMonCat\big)$$$

Lean4

/-- The forgetful functor from semirings to additive commutative monoids preserves all limits.
-/
instance forget₂AddCommMon_preservesLimitsOfSize [UnivLE.{v, u}] :
    PreservesLimitsOfSize.{w, v} (forget₂ SemiRingCat AddCommMonCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F) (forget₂AddCommMonPreservesLimitsAux F) }

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