mathlib documentation


Abelian categories with enough projectives have projective resolutions #

When 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 X.

When C is abelian, projective.d f and f are exact.

Our goal is to define ProjectiveResolution.of Z : ProjectiveResolution Z. The 0-th object in this resolution will just be projective.over Z, i.e. an arbitrarily chosen projective object with a map to Z. After that, we build the n+1-st object as projective.syzygies applied to the previously constructed morphism, and the map to the n-th object as projective.d.

Auxiliary definition for ProjectiveResolution.of.