mathlib4

mathlib4 copied to clipboard

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.

---

• [x] depends on: #12785

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12785~~ By Dependent Issues (🤖). Happy coding!

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

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

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

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.

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 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.

Thanks :tada:

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style