Commit 2021-05-31 13:18 7fe456d8View on Github →
feat(algebra/homology): projective resolutions (#7486)
A projective resolution
P : ProjectiveResolution Z of an object
Z : C consists of
ℕ-indexed chain complex
P.complex of projective objects,
along with a chain map
C to the chain complex consisting just of
Z in degree zero,
so that the augmented chain complex is exact.
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
one will assume
enough_projectives C and
This construction appears in
We show that give
P : ProjectiveResolution X and
Q : ProjectiveResolution Y,
X ⟶ Y admits a lift to a chain map
P.complex ⟶ Q.complex.
(It is a lift in the sense that
the projection maps
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.