hasLimitsOfShape — Mathlib

English

Let J be a small category. Then the category GrpCat has limits of shape J; i.e., for every functor F : J ⥤ GrpCat there exists a limit cone in GrpCat of shape J.

Русский

Пусть J — малая категория. Тогда у GrpCat существуют пределы формы J; то есть для каждого functor F : J ⥤ GrpCat существует предел по форме J в GrpCat.

LaTeX

$$$ \forall J\, (\Small\,J\Rightarrow \mathrm{HasLimitsOfShape}(J, \mathrm{GrpCat}))$$$

Lean4

/-- If `J` is `u`-small, `GrpCat.{u}` has limits of shape `J`. -/
@[to_additive /-- If `J` is `u`-small, `AddGrpCat.{u}` has limits of shape `J`. -/
    ]
instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J GrpCat.{u} where has_limit _ := inferInstance

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