forget₂AddCommGroup_preservesLimitsOfSize

English

The forgetful functor from rings to additive commutative groups preserves all limits.

Русский

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

LaTeX

$$$\mathrm{forget}_2: \text{RingCat} \to \text{AddCommGrpCat}$ preserves limits of size.$$

Lean4

/-- The forgetful functor from rings to additive commutative groups preserves all limits.
-/
instance forget₂AddCommGroup_preservesLimitsOfSize [UnivLE.{v, u}] :
    PreservesLimitsOfSize.{v, v} (forget₂ RingCat.{u} AddCommGrpCat.{u}) where
  preservesLimitsOfShape
    {_
      _} :=
    {
      preservesLimit := fun {F} =>
        preservesLimit_of_preserves_limit_cone (limitConeIsLimit.{v, u} F) (forget₂AddCommGroupPreservesLimitsAux F) }

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