[Merged by Bors] - feat(CategoryTheory): right derived functors

[joelriou]

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.

---

• depends on: [Merged by Bors] - feat(CategoryTheory): transport Kan extensions via equivalences #12785

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): transport Kan extensions via equivalences #12785
  By Dependent Issues (🤖). Happy coding!

[erdOne]

Do we have left derived functors yet?
Thanks Joël and Dagur
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[jcommelin]

How does this mesh with Mathlib/CategoryTheory/Abelian/RightDerived.lean?

[joelriou]

How does this mesh with Mathlib/CategoryTheory/Abelian/RightDerived.lean?

Eventually, Abelian.RightDerived will be refactored (as in my draft branch https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean#L207 ), but we need more material: derived categories, the injective derivability structure, existence of derived functors from derivability structures, etc.

Do we have left derived functors yet?

No, but I would rather develop the right side more before dualising the results.

[jcommelin]

How does this mesh with Mathlib/CategoryTheory/Abelian/RightDerived.lean?

Eventually, Abelian.RightDerived will be refactored (as in my draft branch https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/DerivedCategory/RightDerivedFunctorPlus.lean#L207 ), but we need more material: derived categories, the injective derivability structure, existence of derived functors from derivability structures, etc.

@joelriou could you please explain this in a comment in both files? Then people can be aware of the dual development of the theory for the time being.

[joelriou]

@joelriou could you please explain this in a comment in both files? Then people can be aware of the dual development of the theory for the time being.

Thanks for the suggestion. I have just added TODO in the relevant files.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style