feat(category_theory/preadditive): projective iff coyoneda.obj preser…

…ves epimorphisms (#14832)

src/category_theory/preadditive/injective.lean

@@ -161,6 +161,19 @@ instance {P : C} [projective P] : injective (op P) :=
 { factors := λ X Y g f mono, by exactI ⟨(@projective.factor_thru C _ P _ _ _ g.unop f.unop _).op,
     quiver.hom.unop_inj (by simp)⟩ }
 
+lemma injective_iff_projective_op {J : C} : injective J ↔ projective (op J) :=
+⟨λ h, by exactI infer_instance, λ h, show injective (unop (op J)), by exactI infer_instance⟩
+
+lemma projective_iff_injective_op {P : C} : projective P ↔ injective (op P) :=
+⟨λ h, by exactI infer_instance, λ h, show projective (unop (op P)), by exactI infer_instance⟩
+
+lemma injective_iff_preserves_epimorphisms_yoneda_obj (J : C) :
+  injective J ↔ (yoneda.obj J).preserves_epimorphisms :=
+begin
+  rw [injective_iff_projective_op, projective.projective_iff_preserves_epimorphisms_coyoneda_obj],
+  exact functor.preserves_epimorphisms.iso_iff (coyoneda.obj_op_op _)
+end
+
 section enough_injectives
 variable [enough_injectives C]
 

src/category_theory/preadditive/projective.lean

@@ -26,6 +26,7 @@ noncomputable theory
 
 open category_theory
 open category_theory.limits
+open opposite
 
 universes v u
 
@@ -126,6 +127,13 @@ instance {β : Type v} (g : β → C) [has_zero_morphisms C] [has_biproduct g]
 { factors := λ E X' f e epi, by exactI
   ⟨biproduct.desc (λ b, factor_thru (biproduct.ι g b ≫ f) e), by tidy⟩, }
 
+lemma projective_iff_preserves_epimorphisms_coyoneda_obj (P : C) :
+  projective P ↔ (coyoneda.obj (op P)).preserves_epimorphisms :=
+⟨λ hP, ⟨λ X Y f hf, (epi_iff_surjective _).2 $ λ g, have projective (unop (op P)), from hP,
+  by exactI ⟨factor_thru g f, factor_thru_comp _ _⟩⟩,
+ λ h, ⟨λ E X f e he, by exactI (epi_iff_surjective _).1
+  (infer_instance : epi ((coyoneda.obj (op P)).map e)) f⟩⟩
+
 section enough_projectives
 variables [enough_projectives C]