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(algebra/homology): projective resolutions #7486
Conversation
…ntially surjective
🎉 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! |
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.
I think my biggest question is whether in practical situations we won't get annoyed by the fact that Z
is stuck into this single\0
complex.
Do you think it makes sense to write some machinery to go back and forth between "map of complexes to single\0
" and "map from obj in degree 0
to Z
"?
We already have this machinery, see Moreover, I think later we may be happy to have this formulation, as it's closer to the "(co)fibrant replacement" picture. |
Co-authored-by: Johan Commelin <johan@commelin.net>
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.
Thanks 🎉
bors merge
# Projective resolutions A projective resolution `P : ProjectiveResolution Z` of an object `Z : C` consists of a `ℕ`-indexed chain complex `P.complex` of projective objects, along with a chain map `P.π` from `C` to the chain complex consisting just of `Z` in degree zero, so that the augmented chain complex is exact. When `C` is abelian, this exactness condition is equivalent to `π` being a quasi-isomorphism. It turns out that this formulation allows us to set up the basic theory derived functors without even assuming `C` is abelian. (Typically, however, to show `has_projective_resolutions C` one will assume `enough_projectives C` and `abelian C`. This construction appears in `category_theory.abelian.projectives`.) We show that give `P : ProjectiveResolution X` and `Q : ProjectiveResolution Y`, any morphism `X ⟶ Y` admits a lift to a chain map `P.complex ⟶ Q.complex`. (It is a lift in the sense that the projection maps `P.π` and `Q.π` intertwine the lift and the original morphism.) Moreover, we show that any two such lifts are homotopic. As a consequence, if every object admits a projective resolution, we can construct a functor `projective_resolutions C : C ⥤ homotopy_category C`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Build failed (retrying...): |
# Projective resolutions A projective resolution `P : ProjectiveResolution Z` of an object `Z : C` consists of a `ℕ`-indexed chain complex `P.complex` of projective objects, along with a chain map `P.π` from `C` to the chain complex consisting just of `Z` in degree zero, so that the augmented chain complex is exact. When `C` is abelian, this exactness condition is equivalent to `π` being a quasi-isomorphism. It turns out that this formulation allows us to set up the basic theory derived functors without even assuming `C` is abelian. (Typically, however, to show `has_projective_resolutions C` one will assume `enough_projectives C` and `abelian C`. This construction appears in `category_theory.abelian.projectives`.) We show that give `P : ProjectiveResolution X` and `Q : ProjectiveResolution Y`, any morphism `X ⟶ Y` admits a lift to a chain map `P.complex ⟶ Q.complex`. (It is a lift in the sense that the projection maps `P.π` and `Q.π` intertwine the lift and the original morphism.) Moreover, we show that any two such lifts are homotopic. As a consequence, if every object admits a projective resolution, we can construct a functor `projective_resolutions C : C ⥤ homotopy_category C`. 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: |
Projective resolutions
A projective resolution
P : ProjectiveResolution Z
of an objectZ : C
consists ofa
ℕ
-indexed chain complexP.complex
of projective objects,along with a chain map
P.π
fromC
to the chain complex consisting just ofZ
in degree zero,so that the augmented chain complex is exact.
When
C
is abelian, this exactness condition is equivalent toπ
being a quasi-isomorphism.It turns out that this formulation allows us to set up the basic theory derived functors
without even assuming
C
is abelian.(Typically, however, to show
has_projective_resolutions C
one will assume
enough_projectives C
andabelian C
.This construction appears in
category_theory.abelian.projectives
.)We show that give
P : ProjectiveResolution X
andQ : ProjectiveResolution Y
,any morphism
X ⟶ Y
admits a lift to a chain mapP.complex ⟶ Q.complex
.(It is a lift in the sense that
the projection maps
P.π
andQ.π
intertwine the lift and the original morphism.)Moreover, we show that any two such lifts are homotopic.
As a consequence, if every object admits a projective resolution,
we can construct a functor
projective_resolutions C : C ⥤ homotopy_category C
.