instCreatesColimitsOfShapeFintypeCatForgetOfFinCategory

English

For any J with SmallCategory and FinCategory structure, FintypeCat has colimits of shape J.

Русский

Для любой J с малой категорией и FinCategory структурами, FintypeCat имеет колимиты формы J.

LaTeX

$$$\\mathrm{HasColimitsOfShape}(J, \\mathrm{FintypeCat})$$$

Lean4

noncomputable instance {J : Type} [SmallCategory J] [FinCategory J] : CreatesColimitsOfShape J (forget FintypeCat) :=
  FintypeCat.inclusionCreatesFiniteColimits

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