forget₂Module_preservesLimitsOfSize

English

The forgetful functor forget: AlgCat(R) → Type preserves all limits of size UnivLE.

Русский

Забывающий функтор forget: AlgCat(R) → Type сохраняет все пределы заданного размера UnivLE.

LaTeX

$$$$\text{PreservesLimitsOfSize}(\text{forget}(\text{AlgCat}(R))).$$$$

Lean4

/-- The forgetful functor from R-algebras to R-modules preserves all limits.
-/
instance forget₂Module_preservesLimitsOfSize [UnivLE.{v, w}] :
    PreservesLimitsOfSize.{t, v} (forget₂ (AlgCat.{w} R) (ModuleCat.{w} R)) where
  preservesLimitsOfShape :=
    {
      preservesLimit := fun {K} ↦
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit K)
          (ModuleCat.HasLimits.limitConeIsLimit (K ⋙ forget₂ (AlgCat.{w} R) (ModuleCat.{w} R))) }

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