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

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

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