createsColimitOfFullyFaithfulOfIso'

Lean4
/-- When `F` is fully faithful, to show that `F` creates the colimit for `K` it suffices to show that
a colimit point is in the essential image of `F`.
-/
def createsColimitOfFullyFaithfulOfIso' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cocone (K ⋙ F)}
    (hl : IsColimit l) (X : C) (i : F.obj X ≅ l.pt) : CreatesColimit K F :=
  createsColimitOfFullyFaithfulOfLift' hl
    { pt := X
      ι :=
        { app := fun j => F.preimage (l.ι.app j ≫ i.inv)
          naturality := fun Y Z f => F.map_injective <| by simpa [← cancel_mono i.hom] using l.w f } }
    (Cocones.ext i fun j => by simp)
      -- Notice however that even if the isomorphism is `Iso.refl _`,
      -- this construction will insert additional identity morphisms in the cocone maps,
      -- so the constructed colimits may not be ideal, definitionally.
Похожие утверждения