chore(category_theory/preadditive/projective): split out two lemmas t…

…o reduce imports (#18688)

Motivated by all the unneeded imports visible in https://tqft.net/mathlib4/2023-03-29/category_theory.monoidal.tor.pdf



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/module/injective.lean

@@ -5,6 +5,7 @@ Authors: Jujian Zhang
 -/
 
 import category_theory.preadditive.injective
+import algebra.category.Module.epi_mono
 import ring_theory.ideal.basic
 import linear_algebra.linear_pmap
 

src/category_theory/abelian/injective.lean

@@ -7,6 +7,7 @@ Authors: Jakob von Raumer
 import category_theory.abelian.exact
 import category_theory.preadditive.injective
 import category_theory.preadditive.yoneda.limits
+import category_theory.preadditive.yoneda.injective
 
 /-!
 # Injective objects in abelian categories

src/category_theory/abelian/projective.lean

@@ -7,6 +7,7 @@ import algebra.homology.quasi_iso
 import category_theory.abelian.homology
 import category_theory.preadditive.projective_resolution
 import category_theory.preadditive.yoneda.limits
+import category_theory.preadditive.yoneda.projective
 
 /-!
 # Abelian categories with enough projectives have projective resolutions

src/category_theory/preadditive/injective.lean

@@ -3,11 +3,7 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang, Kevin Buzzard
 -/
-
-import algebra.homology.exact
-import category_theory.types
 import category_theory.preadditive.projective
-import category_theory.limits.shapes.biproducts
 
 /-!
 # Injective objects and categories with enough injectives
@@ -188,33 +184,6 @@ lemma injective_of_adjoint (adj : L ⊣ R) (J : D) [injective J] : injective $ R
 
 end adjunction
 
-section preadditive
-variables [preadditive C]
-
-lemma injective_iff_preserves_epimorphisms_preadditive_yoneda_obj (J : C) :
-  injective J ↔ (preadditive_yoneda.obj J).preserves_epimorphisms :=
-begin
-  rw injective_iff_preserves_epimorphisms_yoneda_obj,
-  refine ⟨λ (h : (preadditive_yoneda.obj J ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
-  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_yoneda.obj J)
-      (forget _) },
-  { introI,
-    exact (infer_instance : (preadditive_yoneda.obj J ⋙ forget _).preserves_epimorphisms) }
-end
-
-lemma injective_iff_preserves_epimorphisms_preadditive_yoneda_obj' (J : C) :
-  injective J ↔ (preadditive_yoneda_obj J).preserves_epimorphisms :=
-begin
-  rw injective_iff_preserves_epimorphisms_yoneda_obj,
-  refine ⟨λ (h : (preadditive_yoneda_obj J ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
-  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_yoneda_obj J)
-      (forget _) },
-  { introI,
-    exact (infer_instance : (preadditive_yoneda_obj J ⋙ forget _).preserves_epimorphisms) }
-end
-
-end preadditive
-
 section enough_injectives
 variable [enough_injectives C]
 

src/category_theory/preadditive/opposite.lean

@@ -3,7 +3,6 @@ Copyright (c) 2021 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Adam Topaz, Johan Commelin, Joël Riou
 -/
-import category_theory.preadditive.basic
 import category_theory.preadditive.additive_functor
 import logic.equiv.transfer_instance
 

src/category_theory/preadditive/projective.lean

@@ -4,12 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 -/
 import algebra.homology.exact
-import category_theory.types
 import category_theory.limits.shapes.biproducts
 import category_theory.adjunction.limits
-import category_theory.preadditive.yoneda.basic
-import algebra.category.Group.epi_mono
-import algebra.category.Module.epi_mono
+import category_theory.limits.preserves.finite
 
 /-!
 # Projective objects and categories with enough projectives
@@ -140,33 +137,6 @@ lemma projective_iff_preserves_epimorphisms_coyoneda_obj (P : C) :
  λ h, ⟨λ E X f e he, by exactI (epi_iff_surjective _).1
   (infer_instance : epi ((coyoneda.obj (op P)).map e)) f⟩⟩
 
-section preadditive
-variables [preadditive C]
-
-lemma projective_iff_preserves_epimorphisms_preadditive_coyoneda_obj (P : C) :
-  projective P ↔ (preadditive_coyoneda.obj (op P)).preserves_epimorphisms :=
-begin
-  rw projective_iff_preserves_epimorphisms_coyoneda_obj,
-  refine ⟨λ (h : (preadditive_coyoneda.obj (op P) ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
-  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_coyoneda.obj (op P))
-      (forget _) },
-  { introI,
-    exact (infer_instance : (preadditive_coyoneda.obj (op P) ⋙ forget _).preserves_epimorphisms) }
-end
-
-lemma projective_iff_preserves_epimorphisms_preadditive_coyoneda_obj' (P : C) :
-  projective P ↔ (preadditive_coyoneda_obj (op P)).preserves_epimorphisms :=
-begin
-  rw projective_iff_preserves_epimorphisms_coyoneda_obj,
-  refine ⟨λ (h : (preadditive_coyoneda_obj (op P) ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
-  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_coyoneda_obj (op P))
-      (forget _) },
-  { introI,
-    exact (infer_instance : (preadditive_coyoneda_obj (op P) ⋙ forget _).preserves_epimorphisms) }
-end
-
-end preadditive
-
 section enough_projectives
 variables [enough_projectives C]
 

src/category_theory/preadditive/yoneda/injective.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Scott Morrison
+-/
+import category_theory.preadditive.yoneda.basic
+import category_theory.preadditive.injective
+import algebra.category.Group.epi_mono
+import algebra.category.Module.epi_mono
+
+/-!
+An object is injective iff the preadditive yoneda functor on it preserves epimorphisms.
+-/
+
+universes v u
+
+open opposite
+
+namespace category_theory
+variables {C : Type u} [category.{v} C]
+
+section preadditive
+variables [preadditive C]
+
+namespace injective
+
+lemma injective_iff_preserves_epimorphisms_preadditive_yoneda_obj (J : C) :
+  injective J ↔ (preadditive_yoneda.obj J).preserves_epimorphisms :=
+begin
+  rw injective_iff_preserves_epimorphisms_yoneda_obj,
+  refine ⟨λ (h : (preadditive_yoneda.obj J ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
+  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_yoneda.obj J)
+      (forget _) },
+  { introI,
+    exact (infer_instance : (preadditive_yoneda.obj J ⋙ forget _).preserves_epimorphisms) }
+end
+
+lemma injective_iff_preserves_epimorphisms_preadditive_yoneda_obj' (J : C) :
+  injective J ↔ (preadditive_yoneda_obj J).preserves_epimorphisms :=
+begin
+  rw injective_iff_preserves_epimorphisms_yoneda_obj,
+  refine ⟨λ (h : (preadditive_yoneda_obj J ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
+  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_yoneda_obj J)
+      (forget _) },
+  { introI,
+    exact (infer_instance : (preadditive_yoneda_obj J ⋙ forget _).preserves_epimorphisms) }
+end
+
+end injective
+
+end preadditive
+
+end category_theory

src/category_theory/preadditive/yoneda/projective.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Scott Morrison
+-/
+import category_theory.preadditive.yoneda.basic
+import category_theory.preadditive.projective
+import algebra.category.Group.epi_mono
+import algebra.category.Module.epi_mono
+
+/-!
+An object is projective iff the preadditive coyoneda functor on it preserves epimorphisms.
+-/
+
+universes v u
+
+open opposite
+
+namespace category_theory
+variables {C : Type u} [category.{v} C]
+
+section preadditive
+variables [preadditive C]
+
+namespace projective
+
+lemma projective_iff_preserves_epimorphisms_preadditive_coyoneda_obj (P : C) :
+  projective P ↔ (preadditive_coyoneda.obj (op P)).preserves_epimorphisms :=
+begin
+  rw projective_iff_preserves_epimorphisms_coyoneda_obj,
+  refine ⟨λ (h : (preadditive_coyoneda.obj (op P) ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
+  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_coyoneda.obj (op P))
+      (forget _) },
+  { introI,
+    exact (infer_instance : (preadditive_coyoneda.obj (op P) ⋙ forget _).preserves_epimorphisms) }
+end
+
+lemma projective_iff_preserves_epimorphisms_preadditive_coyoneda_obj' (P : C) :
+  projective P ↔ (preadditive_coyoneda_obj (op P)).preserves_epimorphisms :=
+begin
+  rw projective_iff_preserves_epimorphisms_coyoneda_obj,
+  refine ⟨λ (h : (preadditive_coyoneda_obj (op P) ⋙ (forget _)).preserves_epimorphisms), _, _⟩,
+  { exactI functor.preserves_epimorphisms_of_preserves_of_reflects (preadditive_coyoneda_obj (op P))
+      (forget _) },
+  { introI,
+    exact (infer_instance : (preadditive_coyoneda_obj (op P) ⋙ forget _).preserves_epimorphisms) }
+end
+
+end projective
+
+end preadditive
+
+end category_theory