instHasColimitsOfShapeOfFinCategory

English

For every ring k and every finite category J, FGModuleCat(k) has colimits of shape J.

Русский

Для любого кольца k и любой конечной категории J FGModuleCat(k) существует колимит по форме J.

LaTeX

$$$\operatorname{HasColimitsOfShape}(J, FGModuleCat(k))$$$

Lean4

instance (J : Type) [Category J] [FinCategory J] : HasColimitsOfShape J (FGModuleCat.{v} k) :=
  hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape (forget₂ (FGModuleCat k) (ModuleCat.{v} k))

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