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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(P : C)
[hP : CategoryTheory.Projective P]
:
(CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(P : C)
[hP : CategoryTheory.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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(P : C)
[hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P))]
:
An object is projective if its preadditive Co-Yoneda functor preserves finite colimits.