English
If G preserves coequalizers and coproducts, then G preserves all colimits (i.e., cocontinuous).
Русский
Если функтор G сохраняет коэквалайзеры и копроизведения, то он сохраняет все колимиты (коконтинуальный).
LaTeX
$$$\forall J\,\forall F : J \to C,\ G(\operatorname{colim}_J F) \cong \operatorname{colim}_J (G \circ F).$$$
Lean4
/-- If G preserves coequalizers and coproducts, it preserves all colimits. -/
theorem preservesColimits_of_preservesCoequalizers_and_coproducts [HasCoequalizers C] [HasCoproducts.{w} C] (G : C ⥤ D)
[PreservesColimitsOfShape WalkingParallelPair G] [∀ J, PreservesColimitsOfShape (Discrete.{w} J) G] :
PreservesColimitsOfSize.{w, w} G where
preservesColimitsOfShape := preservesColimit_of_preservesCoequalizers_and_coproduct G
