English
If G preserves the initial object and pushouts, then G preserves all finite colimits.
Русский
Если функтор G сохраняет начальный объект и пуш-ауты, то G сохраняет все конечные колимиты.
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 initial objects and pushouts, it preserves all finite colimits. -/
theorem preservesFiniteColimits_of_preservesInitial_and_pushouts [HasInitial C] [HasPushouts C] (G : C ⥤ D)
[PreservesColimitsOfShape (Discrete.{0} PEmpty) G] [PreservesColimitsOfShape WalkingSpan G] :
PreservesFiniteColimits G :=
by
haveI : HasFiniteColimits C := hasFiniteColimits_of_hasInitial_and_pushouts
haveI : PreservesColimitsOfShape (Discrete WalkingPair) G :=
preservesBinaryCoproducts_of_preservesInitial_and_pushouts G
haveI : PreservesColimitsOfShape (WalkingParallelPair) G :=
(preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts G)
refine @preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts _ _ _ _ _ _ G _ ?_
refine ⟨fun _ ↦ ?_⟩
apply preservesFiniteCoproductsOfPreservesBinaryAndInitial G
