isColimitCoconeOfIsLeftKanExtension

Lean4
/-- If `c` is a colimit cocone for a functor `F : C ⥤ H` and `α : F ⟶ L ⋙ F'` is the unit of any
left Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coconeOfIsLeftKanExtension α c` is
a colimit cocone, too. -/
@[simps]
noncomputable def isColimitCoconeOfIsLeftKanExtension {c : Cocone F} (hc : IsColimit c) :
    IsColimit (F'.coconeOfIsLeftKanExtension α c)
    where
  desc s := hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))
  fac
    s :=
    by
    have :
      F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫
          (Functor.const _).map (hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))) =
        s.ι :=
      F'.hom_ext_of_isLeftKanExtension α _ _ (by cat_disch)
    exact congr_app this
  uniq s m
    hm :=
    hc.hom_ext
      (fun j ↦ by
        have := hm (L.obj j)
        nth_rw 1 [← F'.descOfIsLeftKanExtension_fac_app α ((const D).obj c.pt)]
        dsimp at this ⊢
        rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app])
Похожие утверждения