mathlib3 documentation

category_theory.preadditive.yoneda.injective

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An object is injective iff the preadditive yoneda functor on it preserves epimorphisms.

theorem category_theory.injective.injective_iff_preserves_epimorphisms_preadditive_yoneda_obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (J : C) :

category_theory.injective J ↔ (category_theory.preadditive_yoneda.obj J).preserves_epimorphisms

theorem category_theory.injective.injective_iff_preserves_epimorphisms_preadditive_yoneda_obj' {C : Type u} [category_theory.category C] [category_theory.preadditive C] (J : C) :

category_theory.injective J ↔ (category_theory.preadditive_yoneda_obj J).preserves_epimorphisms