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.

def CategoryTheory.preservesFiniteColimitsPreadditiveYonedaObjOfInjective {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

• CategoryTheory.preservesFiniteColimitsPreadditiveYonedaObjOfInjective J = (CategoryTheory.preadditiveYonedaObj J).preservesFiniteColimitsOfPreservesEpisAndKernels

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.