mathlib3 documentation

category_theory.preadditive.yoneda.projective

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

An object is projective iff the preadditive coyoneda functor on it preserves epimorphisms.

theorem category_theory.projective.projective_iff_preserves_epimorphisms_preadditive_coyoneda_obj {C : Type u} [category_theory.category C] [category_theory.preadditive C] (P : C) :

category_theory.projective P ↔ (category_theory.preadditive_coyoneda.obj (opposite.op P)).preserves_epimorphisms

theorem category_theory.projective.projective_iff_preserves_epimorphisms_preadditive_coyoneda_obj' {C : Type u} [category_theory.category C] [category_theory.preadditive C] (P : C) :

category_theory.projective P ↔ (category_theory.preadditive_coyoneda_obj (opposite.op P)).preserves_epimorphisms