forget_preservesLimitsOfSize — Mathlib

English

The forgetful functor forget: ModuleCat R → Type preserves limits of size, under a size bound.

Русский

Функтор забывания ModuleCat R → Type сохраняет пределы заданного размера при ограничении по размеру.

LaTeX

$$$\text{PreservesLimitsOfSize}(\text{forget}(\mathrm{ModuleCat}\,R))$$$

Lean4

/-- The forgetful functor from R-modules to types preserves all limits.
-/
instance forget_preservesLimitsOfSize [UnivLE.{v, w}] : PreservesLimitsOfSize.{t, v} (forget (ModuleCat.{w} R)) where
  preservesLimitsOfShape :=
    {
      preservesLimit := fun {K} ↦
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit K) (Types.Small.limitConeIsLimit.{v} (_ ⋙ forget _)) }

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