Commit 2025-07-15 17:59 e2292a32

feat(CategoryTheory/Adjunction): the right partial adjoint (#27168) Given a functor F : C ⥤ D, we define a functor F.partialLeftAdjoint : F.PartialLeftAdjointSource ⥤ C which is defined on a certain full subcategory of D. It satisfies similar properties to the right adjoint of F (if this existed). We show that the domain of definition of this partial right adjoint is stable under certain limits. This dualises #17388, I came across this while formalising Proposition 4.3.4 of Emily Riehl's Category Theory in Context. I will also work on formalising Proposition 4.3.6, which is the bifunctor version of this.