Injective objects in abelian categories #
- Objects in an abelian category are injective if and only if the preadditive Yoneda functor on them preserves finite colimits.
instance CategoryTheory.preservesHomology_preadditiveYonedaObj_of_injective {C : Type u} [Category.{v, u} C] [Abelian C] (J : C) [hJ : Injective J] :
The preadditive Yoneda functor on J preserves homology if J is injective.
instance CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective {C : Type u} [Category.{v, u} C] [Abelian C] (J : C) [hP : Injective J] :
The preadditive Yoneda functor on J preserves colimits if J is injective.
theorem CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj {C : Type u} [Category.{v, u} C] [Abelian C] (J : C) [hP : Limits.PreservesFiniteColimits (preadditiveYonedaObj J)] :
An object is injective if its preadditive Yoneda functor preserves finite colimits.