English
Let C be a category with coequalizers and finite coproducts. If G: C → D preserves coequalizers and finite coproducts, and preserves colimits of shape WalkingParallelPair, then G preserves all finite colimits.
Русский
Пусть C — категория, в которой существуют коэквалайзеры и конечные копроизведения. Если F: C → D сохраняет коэквалайзеры и конечные копроизведения и сохраняет колимиты формы WalkingParallelPair, то F сохраняет все конечные колимиты.
LaTeX
$$$\forall J \text{ finite},\ \forall F : J \to C,\ G(\operatorname{colim}_J F) \cong \operatorname{colim}_J (G \circ F).$$$
Lean4
/-- If G preserves coequalizers and finite coproducts, it preserves finite colimits. -/
theorem preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts [HasCoequalizers C]
[HasFiniteCoproducts C] (G : C ⥤ D) [PreservesColimitsOfShape WalkingParallelPair G] [PreservesFiniteCoproducts G] :
PreservesFiniteColimits G where
preservesFiniteColimits := by
intro J sJ fJ
apply preservesColimit_of_preservesCoequalizers_and_coproduct
