forget₂Group_preservesLimits — Mathlib

English

The forgetful functor from commutative groups to groups preserves limits of all shapes; i.e., for every diagram F: J → CommGrpCat, the limit in GrpCat is computed by forgetting the commutative structure from the limit in CommGrpCat.

Русский

Функтор забывания из коммутативных групп в группы сохраняет пределы всех форм; то есть для каждого диаграммы F: J → CommGrpCat предел в GrpCat получается из предела в CommGrpCat путём забывания коммутативной структуры.

LaTeX

$$$\\operatorname{PreservesLimits}(\\mathrm{forget}_{CommGrpCat\\to GrpCat})$$$

Lean4

@[to_additive]
instance forget₂Group_preservesLimits : PreservesLimits (forget₂ CommGrpCat GrpCat.{u}) :=
  CommGrpCat.forget₂Group_preservesLimitsOfSize.{u, u}

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