Documentation

Mathlib.CategoryTheory.Abelian.Projective

Projective objects in abelian categories #

In an abelian category, an object P is projective iff the functor preadditiveCoyonedaObj (op P) preserves finite colimits.

The preadditive Co-Yoneda functor on P preserves homology if P is projective.

Equations