Commit 2026-10-31 10:05 c2583912

refactor(CategoryTheory): colimits of representable presheaves (#42816) The file Mathlib/CategoryTheory/Limits/Presheaf.lean has already been refactored a few times. This PR is an effort in order to cleanup this file which contains various results about presheaves of types which should be organized better. All the definitions in Limits/Presheaf.lean have been moved or deprecated. The fact that a presheaf of types is a colimit of representable presheaves is now in the file Functor/KanExtension/DenseAtYoneda.lean. The results are stated using cocones indexed by (the opposite) of a category of elements, but they are also stated as the density of the Yoneda embedding (Functor.IsDense). We prove the results first for the most general version of the Yoneda embedding which is shrinkYoneda, and we deduce similar results for uliftYoneda and yoneda. (Some dual versions are also obtained in the file Functor/KanExtension/DenseAtCoyoneda.lean). Results about left Kan extensions along the Yoneda embedding are obtained in the file Functor/KanExtension/RestrictedYoneda.lean, and an application is obtained in the file Functor/KanExtension/RestrictedYoneda.lean: if F is a functor between locally w-small categories, we have the isomorphism F ⋙ shrinkYoneda.{w} ≅ shrinkYoneda.{w} ⋙ F.op.lan, which makes F.op.lan a left Kan extension of F ⋙ shrinkYoneda.{w} along the Yoneda embedding. (Doing so required splitting the file Dense.lean. New files DenseIff.lean and StrongGenerator.lean contain respectively a characterization of dense functors in terms of the restricted Yoneda functors, and the fact that the image of a dense functor is a strong generator.)