has_colimits_of_hasCoequalizers_and_coproducts

English

If appropriate colimits exist, then there is a colimit for F.

Русский

При условии существования нужных колимитов существует колимит для F.

LaTeX

$$HasColimit F$$

Lean4

/-- Any category with coproducts and coequalizers has all colimits. -/
@[stacks 002P]
theorem has_colimits_of_hasCoequalizers_and_coproducts [HasCoproducts.{w} C] [HasCoequalizers C] :
    HasColimitsOfSize.{w, w} C where
  has_colimits_of_shape := fun _ _ => { has_colimit := fun F => hasColimit_of_coequalizer_and_coproduct F }

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