forget₂Ring_preservesLimitsOfSize

English

The category of commutative rings has all limits.

Русский

Категория коммутативных колец имеет все пределы.

LaTeX

$$$\mathrm{HasLimits}(\mathrm{CommRingCat})$$$

Lean4

/-- The forgetful functor from commutative rings to rings preserves all limits.
(That is, the underlying rings could have been computed instead as limits in the category of rings.)
-/
instance forget₂Ring_preservesLimitsOfSize [UnivLE.{v, u}] :
    PreservesLimitsOfSize.{w, v} (forget₂ CommRingCat RingCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone.{w, v} (limitConeIsLimit.{v, u} F) (RingCat.limitConeIsLimit.{v, u} _) }

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