Injective objects in abelian categories #
- Objects in an abelian categories 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]
:
(preadditiveYonedaObj J).PreservesHomology
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.