createsFiniteColimitsOfCreatesInitialAndPushouts

Lean4
/-- If a functor creates initial objects and pushouts, it creates finite 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 createsFiniteColimitsOfCreatesInitialAndPushouts [HasInitial D] [HasPushouts D] (G : C ⥤ D)
    [G.ReflectsIsomorphisms] [CreatesColimitsOfShape (Discrete.{0} PEmpty) G] [CreatesColimitsOfShape WalkingSpan G] :
    CreatesFiniteColimits G where
  createsFiniteColimits _ _
    _ :=
    {
      CreatesColimit :=
        have : HasInitial C := hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape G
        have : HasPushouts C := hasColimitsOfShape_of_hasColimitsOfShape_createsColimitsOfShape G
        have : HasFiniteColimits C := hasFiniteColimits_of_hasInitial_and_pushouts
        createsColimitOfReflectsIsomorphismsOfPreserves }
Похожие утверждения