Commit 2024-06-05 12:48 77504eef
View on Github →feat(CategoryTheory): right derived functors (#12788)
In this PR, given a functor F : C ⥤ H, and L : C ⥤ D that is a localization functor for W : MorphismProperty C, we define F.totalRightDerived L W : D ⥤ H as the left Kan extension of F along L: it is defined if the type class F.HasRightDerivedFunctor W asserting the existence of a left Kan extension is satisfied.