mathlib documentation

category_theory.abelian.projective

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.

Equations
@[irreducible]

In any abelian category with enough projectives, ProjectiveResolution.of Z constructs a projective resolution of the object Z.

Equations