Commit 2024-10-23 02:43 c48f8a2c

feat(CategoryTheory/Adjunction): the left partial adjoint (#17388) Given a functor F : D ⥤ C, we define a functorF.partialLeftAdjoint : F.PartialLeftAdjointSource ⥤ D which is defined on a certain full subcategory of C. It satisfies similar properties to the left adjoint of F (if this existed). We show that the domain of definition of this partial left adjoint is stable under certain colimits. This shall be used in #17366 in order to show the existence of the pullback functor on categories of presheaves of modules.