forget_preservesLimitsOfSize — Mathlib

English

The forgetful functor forget₂ from SemiRingCat to MonCat preserves all limits of shape, via a small-section reduction.

Русский

Забывающий функтор forget₂: SemiRingCat → MonCat сохраняет все пределы формы, через редукцию к малому числу секций.

LaTeX

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

Lean4

/-- The forgetful functor from semirings to types preserves all limits.
-/
instance forget_preservesLimitsOfSize [UnivLE.{v, u}] : PreservesLimitsOfSize.{w, v} (forget SemiRingCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit F)
          (Types.Small.limitConeIsLimit.{v, u} (F ⋙ forget _)) }

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