createsColimitOfFullyFaithfulOfLift'

Lean4

/-- When `F` is fully faithful, to show that `F` creates the colimit for `K` it suffices to exhibit a
lift of a colimit cocone for `K ⋙ F`.
-/
def createsColimitOfFullyFaithfulOfLift' {K : J ⥤ C} {F : C ⥤ D} [F.Full] [F.Faithful] {l : Cocone (K ⋙ F)}
    (hl : IsColimit l) (c : Cocone K) (i : F.mapCocone c ≅ l) : CreatesColimit K F :=
  createsColimitOfReflectsIso' hl
    ⟨⟨c, i⟩, isColimitOfReflects F (IsColimit.ofIsoColimit hl i.symm)⟩
      -- 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.

Похожие утверждения