Abelian categories with enough projectives have projective resolutions #
C is abelian
Projective.d f and
f are exact.
Hence, starting from an epimorphism
P ⟶ X, where
P is projective,
we can apply
Projective.d repeatedly to obtain a projective resolution of
The preadditive Co-Yoneda functor on
P preserves colimits if
P is projective.
An object is projective if its preadditive Co-Yoneda functor preserves finite colimits.
Our goal is to define
ProjectiveResolution.of Z : ProjectiveResolution Z.
0-th object in this resolution will just be
i.e. an arbitrarily chosen projective object with a map to
After that, we build the
n+1-st object as
applied to the previously constructed morphism,
and the map to the
n-th object as
In any abelian category with enough projectives,
ProjectiveResolution.of Z constructs a projective resolution of the object
X is a chain complex of projective objects and we have a quasi-isomorphism
f : X ⟶ Y,
X is a projective resolution of