Projective objects in abelian categories #
In an abelian category, an object P is projective iff the functor
preadditiveCoyonedaObj (op 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 (Opposite.op 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]
:
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 (Opposite.op P))]
:
An object is projective if its preadditive Co-Yoneda functor preserves finite colimits.