forget_preservesLimitsOfSize — Mathlib

English

The forget₂ forgetful functor from AlgCat(R) to ModuleCat(R) preserves all limits.

Русский

Забывающий функтор forget₂ AlgCat(R) → ModuleCat(R) сохраняет все пределы.

LaTeX

$$$$\text{PreservesLimits}(\text{forget₂}(\text{AlgCat}(R), \text{ModuleCat}(R))).$$$$

Lean4

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

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