An object is projective iff the preadditive coyoneda functor on it preserves epimorphisms.

theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : C) : CategoryTheory.Projective P ↔ CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.preadditiveCoyoneda.toPrefunctor.obj (Opposite.op P))

theorem CategoryTheory.Projective.projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (P : C) : CategoryTheory.Projective P ↔ CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.preadditiveCoyoneda.toPrefunctor.obj (Opposite.op P))