Lean4
/-- If `F` reflects isomorphisms and we can lift any limit cone to a limit cone,
then `F` creates limits.
In particular here we don't need to assume that F reflects limits.
-/
def createsLimitOfReflectsIso {K : J ⥤ C} {F : C ⥤ D} [F.ReflectsIsomorphisms] (h : ∀ c t, LiftsToLimit K F c t) :
CreatesLimit K F where
lifts c t := (h c t).toLiftableCone
toReflectsLimit :=
{
reflects := fun {d} hd =>
⟨by
let d' : Cone K := (h (F.mapCone d) hd).toLiftableCone.liftedCone
let i : F.mapCone d' ≅ F.mapCone d := (h (F.mapCone d) hd).toLiftableCone.validLift
let hd' : IsLimit d' := (h (F.mapCone d) hd).makesLimit
let f : d ⟶ d' := hd'.liftConeMorphism d
have : (Cones.functoriality K F).map f = i.inv := (hd.ofIsoLimit i.symm).uniq_cone_morphism
haveI : IsIso ((Cones.functoriality K F).map f) :=
by
rw [this]
infer_instance
haveI : IsIso f := isIso_of_reflects_iso f (Cones.functoriality K F)
exact IsLimit.ofIsoLimit hd' (asIso f).symm⟩ }
