forget₂Ring_preservesLimitsOfSize

English

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

Русский

Функтор забывания forget₂: AlgCat(R) → RingCat сохраняет все пределы заданного размера UnivLE.

LaTeX

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

Lean4

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

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