forget_createsLimitsOfShape — Mathlib

English

The forgetful functor from CommGrpCat to GrpCat creates limits of a given shape: the limit in GrpCat can be obtained from the limit in GrpCat by forgetting the commutativity constraint and then reinterpreting.

Русский

Забывающий функтор CommGrpCat ⥤ GrpCat создаёт пределы заданной формы: предел в GrpCat получается из предела в GrpCat путём забывания коммутивности.

LaTeX

$$$ \text{Forget₂} \text{(CommGrpCat → GrpCat)} \text{ createsLimit } F $$$

Lean4

@[to_additive]
noncomputable instance forget_createsLimitsOfShape : CreatesLimitsOfShape J (forget GrpCat.{u}) where
  CreatesLimit := inferInstance

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