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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(J : C)
[hJ : CategoryTheory.Injective J]
:
(CategoryTheory.preadditiveYonedaObj J).PreservesHomology
The preadditive Yoneda functor on J preserves homology if J is injective.
instance
CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(J : C)
[hP : CategoryTheory.Injective J]
:
The preadditive Yoneda functor on J preserves colimits if J is injective.
theorem
CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
(J : C)
[hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)]
:
An object is injective if its preadditive Yoneda functor preserves finite colimits.