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.preadditiveCoyoneda.obj (Opposite.op P)).PreservesEpimorphisms

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.preadditiveCoyoneda.obj (Opposite.op P)).PreservesEpimorphisms