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.

Equations

• ⋯ = ⋯

instance CategoryTheory.preservesFiniteColimits_preadditiveYonedaObj_of_injective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (J : C) [hP : CategoryTheory.Injective J] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)

The preadditive Yoneda functor on J preserves colimits if J is injective.

Equations

• ⋯ = ⋯

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)] : CategoryTheory.Injective J

An object is injective if its preadditive Yoneda functor preserves finite colimits.