An object is injective iff the preadditive yoneda functor on it preserves epimorphisms.

theorem CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (J : C) : CategoryTheory.Injective J ↔ CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.preadditiveYoneda.toPrefunctor.obj J)

theorem CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditive_yoneda_obj' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (J : C) : CategoryTheory.Injective J ↔ CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.preadditiveYonedaObj J)