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