forget₂Group_preservesLimitsOfSize

English

The forgetful functor forget₂ CommGrpCat GrpCat preserves limits of all sizes.

Русский

Забывающий функтор forget₂ CommGrpCat GrpCat сохраняет пределы любого размера.

LaTeX

$$$ \mathrm{PreservesLimitsOfSize}(\mathrm{forget₂ CommGrpCat GrpCat}) $$$

Lean4

/-- The forgetful functor from commutative groups to groups preserves all limits.
(That is, the underlying group could have been computed instead as limits in the category
of groups.)
-/
@[to_additive (relevant_arg := 100) /--
    The forgetful functor from additive commutative groups to additive groups preserves all
    limits. (That is, the underlying group could have been computed instead as limits  in the
    category of additive groups.) -/
    ]
instance forget₂Group_preservesLimitsOfSize : PreservesLimitsOfSize.{w, v} (forget₂ CommGrpCat.{u} GrpCat.{u}) where

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