feat(CategoryTheory): deriving functors using a right derivability structure#23915
feat(CategoryTheory): deriving functors using a right derivability structure#23915
Conversation
…rivability-structure-pointwise
…re-api' into jriou-pointwise-right-derived-functor
…nctor' into jriou-derivability-structure-pointwise
PR summary 32df3bc130Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
This pull request has conflicts, please merge |
|
This pull request has conflicts, please merge |
|
See #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 Ffor a functorFsaying thatΦ.functor ⋙ Finverts the given class of morphisms, and in caseΦis a right derivability structure, we show thatFadmits 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.)