CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj

theorem CategoryTheory.injective_of_preservesFiniteColimits_preadditiveYonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (J : C) [hP : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.preadditiveYonedaObj J)], CategoryTheory.Injective J

This theorem states that if we have an object 'J' in a category 'C', which is assumed to be both a category and an abelian category, then if the preadditive Yoneda functor of 'J' preserves finite colimits, 'J' is an injective object in 'C'. Here, the preadditive Yoneda functor and the preservation of finite colimits are key concepts in category theory.

More concisely: If 'J' is an object in an abelian category 'C' such that the preadditive Yoneda functor of 'J' preserves finite colimits, then 'J' is an injective object in 'C'.