Commit 2024-07-04 06:28 1345527c

feat(CategoryTheory/Functor): refactoring Lan (#10425) This PR refactors the definition of the left Kan extension functor (Functor.lan : (C ⥤ E) ⥤ (D ⥤ E)) which sends a functor to its left Kan extension along a given functor F : C ⥤ D. This definition used to be a construction based on the existence of suitable colimits. The new definition relies on the new general API for left Kan extensions. Then, F.lan.obj G is now defined as leftKanExtension F G. As a result, (leftKanExtension F G).obj X is no longer defined as colimit, but when it is known that G has a pointwise left Kan extension, it is shown that leftKanExtension F G is indeed a pointwise left Kan extension, which means that (leftKanExtension F G).obj X is the point of a certain colimit cocone. Then, in the downstream applications of this construction we have to use the API for colimit cocones rather that the colimit API. The file CategoryTheory.Limits.Presheaf is also significantly refactored: instead of reconstructing functors by using colimits, we make use of the left Kan extension API. As the pullback of presheaves is a left Kan extension, the file Topology.Sheaves.Presheaf is also refactored: the pushforward and pullback functors are redefined in a more direct manner.