hasFiniteColimits_of_hasInitial_and_pushouts

English

If a category has an initial object and pushouts, then it has all finite colimits.

Русский

Если в категории существует начальный объект и пуш-ауты, то существуют все конечные колимиты.

LaTeX

$$$\text{HasFiniteColimits}(C) \quad\text{provided } \text{HasInitial}(C) \wedge \text{HasPushouts}(C).$$$

Lean4

theorem hasFiniteColimits_of_hasInitial_and_pushouts [HasInitial C] [HasPushouts C] : HasFiniteColimits C :=
  @hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts C _
    (@hasFiniteCoproducts_of_has_binary_and_initial C _ (hasBinaryCoproducts_of_hasInitial_and_pushouts C)
      inferInstance)
    (@hasCoequalizers_of_hasPushouts_and_binary_coproducts C _ (hasBinaryCoproducts_of_hasInitial_and_pushouts C)
      inferInstance)

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