forget₂Mon_preservesLimitsOfSize

English

For a diagram F: J → SemiRingCat, the forgetful functor to MonCat preserves limits of size.

Русский

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

LaTeX

$$$\operatorname{PreservesLimitsOfSize}\big(\operatorname{forget}_2 SemiRingCat MonCat\big)$$$

Lean4

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

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