English
Any category with finite coproducts and coequalizers has all finite colimits.
Русский
Любая категория с конечными копроизведениями и коэквалайзерами имеет все конечные колимиты.
LaTeX
$$$HasFiniteCoproducts C \land HasCoequalizers C \Rightarrow HasFiniteColimits C$$$
Lean4
/-- Any category with finite coproducts and coequalizers has all finite colimits. -/
@[stacks 002Q]
theorem hasFiniteColimits_of_hasCoequalizers_and_finite_coproducts [HasFiniteCoproducts C] [HasCoequalizers C] :
HasFiniteColimits C where out _ := { has_colimit := fun F => hasColimit_of_coequalizer_and_coproduct F }
