hasFiniteColimits_of_hasColimitsOfSize

English

If C has all colimits, it has finite colimits.

Русский

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

LaTeX

$$$\operatorname{HasColimits}(C) \Rightarrow \operatorname{HasFiniteColimits}(C)$$$

Lean4

theorem hasFiniteColimits_of_hasColimitsOfSize [HasColimitsOfSize.{v', u'} C] : HasFiniteColimits C where
  out := fun J hJ hJ' =>
    haveI := hasColimitsOfSizeShrink.{0, 0} C
    let F := @FinCategory.equivAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ'
    @hasColimitsOfShape_of_equivalence (@FinCategory.AsType J (@FinCategory.fintypeObj J hJ hJ'))
      (@FinCategory.categoryAsType J (@FinCategory.fintypeObj J hJ hJ') hJ hJ') _ _ J hJ F _

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