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(category_theory): left-derived functors #7487
Conversation
…ntially surjective
Co-authored-by: Johan Commelin <johan@commelin.net>
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
This reverts commit c368ab3.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM!
bors d+
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Adam Topaz <adamtopaz@users.noreply.github.com>
bors merge |
# Left-derived functors We define the left-derived functors `F.left_derived n : C ⥤ D` for any additive functor `F` out of a category with projective resolutions. The definition is ``` projective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n ``` that is, we pick a projective resolution (thought of as an object of the homotopy category), we apply `F` objectwise, and compute `n`-th homology. We show that these left-derived functors can be calculated on objects using any choice of projective resolution, and on morphisms by any choice of lift to a chain map between chosen projective resolutions. Similarly we define natural transformations between left-derived functors coming from natural transformations between the original additive functors, and show how to compute the components. ## Implementation We don't assume the categories involved are abelian (just preadditive, and have equalizers, cokernels, and image maps), or that the functors are right exact. None of these assumptions are needed yet. It is often convenient, of course, to work with `[abelian C] [enough_projectives C] [abelian D]` which (assuming the results from `category_theory.abelian.projective`) are enough to provide all the typeclass hypotheses assumed here. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded: |
# Left-derived functors We define the left-derived functors `F.left_derived n : C ⥤ D` for any additive functor `F` out of a category with projective resolutions. The definition is ``` projective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n ``` that is, we pick a projective resolution (thought of as an object of the homotopy category), we apply `F` objectwise, and compute `n`-th homology. We show that these left-derived functors can be calculated on objects using any choice of projective resolution, and on morphisms by any choice of lift to a chain map between chosen projective resolutions. Similarly we define natural transformations between left-derived functors coming from natural transformations between the original additive functors, and show how to compute the components. ## Implementation We don't assume the categories involved are abelian (just preadditive, and have equalizers, cokernels, and image maps), or that the functors are right exact. None of these assumptions are needed yet. It is often convenient, of course, to work with `[abelian C] [enough_projectives C] [abelian D]` which (assuming the results from `category_theory.abelian.projective`) are enough to provide all the typeclass hypotheses assumed here. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Left-derived functors
We define the left-derived functors
F.left_derived n : C ⥤ D
for any additive functorF
out of a category with projective resolutions.
The definition is
that is, we pick a projective resolution (thought of as an object of the homotopy category),
we apply
F
objectwise, and computen
-th homology.We show that these left-derived functors can be calculated
on objects using any choice of projective resolution,
and on morphisms by any choice of lift to a chain map between chosen projective resolutions.
Similarly we define natural transformations between left-derived functors coming from
natural transformations between the original additive functors,
and show how to compute the components.
Implementation
We don't assume the categories involved are abelian
(just preadditive, and have equalizers, cokernels, and image maps),
or that the functors are right exact.
None of these assumptions are needed yet.
It is often convenient, of course, to work with
[abelian C] [enough_projectives C] [abelian D]
which (assuming the results from
category_theory.abelian.projective
) are enough toprovide all the typeclass hypotheses assumed here.