Projective objects in abelian categories

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

instance CategoryTheory.preservesHomology_preadditiveCoyonedaObj_of_projective {C : Type u} [Category.{v, u} C] [Abelian C] (P : C) [hP : Projective P] : (preadditiveCoyonedaObj P).PreservesHomology

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

instance CategoryTheory.preservesFiniteColimits_preadditiveCoyonedaObj_of_projective {C : Type u} [Category.{v, u} C] [Abelian C] (P : C) [hP : Projective P] : Limits.PreservesFiniteColimits (preadditiveCoyonedaObj P)

The preadditive co-Yoneda functor on P preserves finite colimits if P is projective.

theorem CategoryTheory.projective_of_preservesFiniteColimits_preadditiveCoyonedaObj {C : Type u} [Category.{v, u} C] [Abelian C] (P : C) [hP : Limits.PreservesFiniteColimits (preadditiveCoyonedaObj P)] : Projective P

An object is projective if its preadditive co-Yoneda functor preserves finite colimits.