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.preadditiveYoneda.obj J).PreservesEpimorphisms

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.preadditiveYonedaObj J).PreservesEpimorphisms