Projective objects in abelian categories

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

noncomputable def CategoryTheory.preservesFiniteColimitsPreadditiveCoyonedaObjOfProjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) [hP : CategoryTheory.Projective P] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveCoyonedaObj { unop := P })

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

Equations

• CategoryTheory.preservesFiniteColimitsPreadditiveCoyonedaObjOfProjective P = (CategoryTheory.preadditiveCoyonedaObj { unop := P }).preservesFiniteColimitsOfPreservesEpisAndKernels

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 { unop := P })] : CategoryTheory.Projective P

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