Projective objects in abelian categories

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

noncomputable instance CategoryTheory.preservesHomologyPreadditiveCoyonedaObjOfProjective {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.

Equations

• CategoryTheory.preservesHomologyPreadditiveCoyonedaObjOfProjective P = (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P)).preservesHomologyOfPreservesEpisAndKernels

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

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

Equations

• CategoryTheory.preservesFiniteColimitsPreadditiveCoyonedaObjOfProjective P = (CategoryTheory.preadditiveCoyonedaObj (Opposite.op P)).preservesFiniteColimitsOfPreservesHomology

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))] : CategoryTheory.Projective P

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