Commit 2025-11-16 19:50 f17d16e5

feat(CategoryTheory): deriving functors using a right derivability structure (#31400) We develop the API for derived functors following the existence theorem obtained in #26374. If Φ is a localizer morphism, we introduce a predicate Φ.Derives F for a functor F saying that Φ.functor ⋙ F inverts the given class of morphisms, and in case Φ is a right derivability structure, we show that F admits a right derived functor, and we obtain a recognition lemma for this derived functor. (In the future, this will be applied to the injective/projective/flat derivability structures.)