forget_createsLimitsOfShape — Mathlib

English

The forgetful functor forget_CommGrpCat to CommMonCat creates limits of shape J.

Русский

Функтор забывания forget_CommGrpCat в CommMonCat порождает пределы формы J.

LaTeX

$$$\\text{forget}_{CommGrpCat\\to CommMonCat}\\;\\text{CreatesLimitsOfShape}\\;J$$$

Lean4

@[to_additive]
noncomputable instance forget_createsLimitsOfShape (J : Type v) [Category.{w} J] :
    CreatesLimitsOfShape J (forget CommGrpCat.{u}) where CreatesLimit := inferInstance

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