English
If G creates coequalizers and the corresponding coproducts, then G creates colimits of shape J for all J.
Русский
Если функтор G создаёт коэквалайзеры и соответствующие копроизведения, он создаёт колимиты формы J для всех J.
LaTeX
$$$\forall J,\ CreatesColimitsOfShape J G.$$$
Lean4
/-- If a functor creates coequalizers and the appropriate coproducts, it creates colimits.
We additionally require the rather strong condition that the functor reflects isomorphisms. It is
unclear whether the statement remains true without this condition. There are various definitions of
"creating colimits" in the literature, and whether or not the condition can be dropped seems to
depend on the specific definition that is used. -/
noncomputable def createsColimitsOfShapeOfCreatesCoequalizersAndCoproducts : CreatesColimitsOfShape J G where
CreatesColimit
{K} :=
have : HasColimitsOfShape (Discrete J) C := hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape G
have : HasColimitsOfShape (Discrete (Σ p : J × J, p.1 ⟶ p.2)) C :=
hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape G
have : HasCoequalizers C := hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape G
have : HasColimit K := hasColimit_of_coequalizer_and_coproduct K
createsColimitOfReflectsIsomorphismsOfPreserves
