Injective objects in abelian categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
- Objects in an abelian categories are injective if and only if the preadditive Yoneda functor on them preserves finite colimits.
noncomputable
def
category_theory.preserves_finite_colimits_preadditive_yoneda_obj_of_injective
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(J : C)
[hP : category_theory.injective J] :
The preadditive Yoneda functor on J preserves colimits if J is injective.
theorem
category_theory.injective_of_preserves_finite_colimits_preadditive_yoneda_obj
{C : Type u}
[category_theory.category C]
[category_theory.abelian C]
(J : C)
[hP : category_theory.limits.preserves_finite_colimits (category_theory.preadditive_yoneda_obj J)] :
An object is injective if its preadditive Yoneda functor preserves finite colimits.