forget₂AddCommGroup_preservesLimitsOfSize

English

The forgetful functor forget₂ from ModuleCat to AddCommGrpCat preserves limits of size, uniformly in size bounds.

Русский

Функтор забывания forget₂ из ModuleCat в AddCommGrpCat сохраняет пределы любого размера в пределах заданного размера.

LaTeX

$$$\text{PreservesLimitsOfSize }(\text{forget₂}(\mathrm{ModuleCat}\,R))$$$

Lean4

/-- The forgetful functor from R-modules to abelian groups preserves all limits.
-/
instance forget₂AddCommGroup_preservesLimitsOfSize [UnivLE.{v, w}] :
    PreservesLimitsOfSize.{t, v} (forget₂ (ModuleCat.{w} R) AddCommGrpCat.{w}) where
  preservesLimitsOfShape := { preservesLimit := inferInstance }

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