hasColimitsOfShape_of_hasFiniteColimits

English

If C has finite colimits, then HasColimitsOfShape J C for finite J.

Русский

Если в C существуют конечные колимиты, то HasColimitsOfShape J C для конечных J существует.

LaTeX

$$$\operatorname{HasFiniteColimits}(C) \Rightarrow \forall J\,[\operatorname{Fin}(J) \Rightarrow \operatorname{HasColimitsOfShape}(J, C)]$$$

Lean4

instance (priority := 100) hasColimitsOfShape_of_hasFiniteColimits [HasFiniteColimits C] (J : Type w) [SmallCategory J]
    [FinCategory J] : HasColimitsOfShape J C :=
  by
  refine @hasColimitsOfShape_of_equivalence _ _ _ _ _ _ (FinCategory.equivAsType J) ?_
  apply HasFiniteColimits.out

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