Injective objects

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

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

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