-
Notifications
You must be signed in to change notification settings - Fork 330
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(CategoryTheory): right derived functors #12788
Conversation
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
This PR/issue depends on: |
Do we have left derived functors yet? |
🚀 Pull request has been placed on the maintainer queue by erdOne. |
How does this mesh with |
Eventually,
No, but I would rather develop the right side more before dualising the results. |
@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 🎉 bors merge |
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. Co-authored-by: Joël Riou <[email protected]>
Pull request successfully merged into master. Build succeeded: |
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. Co-authored-by: Joël Riou <[email protected]>
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. Co-authored-by: Joël Riou <[email protected]>
In this PR, given a functor
F : C ⥤ H
, andL : C ⥤ D
that is a localization functor forW : MorphismProperty C
, we defineF.totalRightDerived L W : D ⥤ H
as the left Kan extension ofF
alongL
: it is defined if the type classF.HasRightDerivedFunctor W
asserting the existence of a left Kan extension is satisfied.