mathlib3 documentation


Abelian categories with enough projectives have projective resolutions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.


If X is a chain complex of projective objects and we have a quasi-isomorphism f : X ⟶ Y[0], then X is a projective resolution of Y.