colimitIsoColimitGrothendieck — Mathlib

Lean4
/-- If `G : C ⥤ H` admits a left Kan extension along a functor `L : C ⥤ D` and `H` has colimits of
shape `C` and `D`, then the colimit of `G` is isomorphic to the colimit of a canonical functor
`Grothendieck (CostructuredArrow.functor L) ⥤ H` induced by `L` and `G`. -/
noncomputable def colimitIsoColimitGrothendieck : colimit G ≅ colimit (CostructuredArrow.grothendieckProj L ⋙ G) :=
  calc
    colimit G ≅ colimit (leftKanExtension L G) := (colimitIsoOfIsLeftKanExtension _ (L.leftKanExtensionUnit G)).symm
    _ ≅ colimit (fiberwiseColimit (CostructuredArrow.grothendieckProj L ⋙ G)) :=
      (HasColimit.isoOfNatIso (leftKanExtensionIsoFiberwiseColimit L G))
    _ ≅ colimit (CostructuredArrow.grothendieckProj L ⋙ G) := colimitFiberwiseColimitIso _
Похожие утверждения