leftKanExtensionIsoFiberwiseColimit

Lean4
/-- The left Kan extension of `F : C ⥤ H` along a functor `L : C ⥤ D` is isomorphic to the
fiberwise colimit of the projection functor on the Grothendieck construction of the costructured
arrow category composed with `F`. -/
@[simps!]
noncomputable def leftKanExtensionIsoFiberwiseColimit [HasLeftKanExtension L F] :
    leftKanExtension L F ≅ fiberwiseColimit (grothendieckProj L ⋙ F) :=
  letI : ∀ X, HasColimit (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F) := fun X =>
    hasColimit_of_iso <|
      Iso.symm <|
        isoWhiskerRight (eqToIso ((functor L).map_id X)) _ ≪≫
          Functor.leftUnitor (Grothendieck.ι (functor L) X ⋙ grothendieckProj L ⋙ F)
  Iso.symm <|
    NatIso.ofComponents
      (fun X =>
        HasColimit.isoOfNatIso (isoWhiskerRight (ιCompGrothendieckProj L X) F) ≪≫
          (leftKanExtensionObjIsoColimit L F X).symm)
      fun f => colimit.hom_ext (by simp)
Похожие утверждения