Lean4
/-- If `F` reflects isomorphisms and we can lift any colimit cocone to a colimit cocone,
then `F` creates colimits.
In particular here we don't need to assume that F reflects colimits.
-/
def createsColimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] (h : ∀ c t, LiftsToColimit K F c t) :
CreatesColimit K F where
lifts c t := (h c t).toLiftableCocone
toReflectsColimit :=
{
reflects := fun {d} hd =>
⟨by
let d' : Cocone K := (h (F.mapCocone d) hd).toLiftableCocone.liftedCocone
let i : F.mapCocone d' ≅ F.mapCocone d := (h (F.mapCocone d) hd).toLiftableCocone.validLift
let hd' : IsColimit d' := (h (F.mapCocone d) hd).makesColimit
let f : d' ⟶ d := hd'.descCoconeMorphism d
have : (Cocones.functoriality K F).map f = i.hom := (hd.ofIsoColimit i.symm).uniq_cocone_morphism
haveI : IsIso ((Cocones.functoriality K F).map f) :=
by
rw [this]
infer_instance
haveI := isIso_of_reflects_iso f (Cocones.functoriality K F)
exact IsColimit.ofIsoColimit hd' (asIso f)⟩ }
