feat(algebra/category): forgetful functors from modules/abelian group…

…s preserve epis/monos (#15108)

The corresponding `reflects` statements already follow from faithfulness.

src/algebra/category/Group/epi_mono.lean

@@ -321,6 +321,19 @@ iff.trans (epi_iff_surjective _) (add_subgroup.eq_top_iff' f.range).symm
 
 end AddGroup
 
+namespace Group
+variables {A B : Group.{u}} (f : A ⟶ B)
+
+@[to_additive]
+instance forget_Group_preserves_mono : (forget Group).preserves_monomorphisms :=
+{ preserves := λ X Y f e, by rwa [mono_iff_injective, ←category_theory.mono_iff_injective] at e }
+
+@[to_additive]
+instance forget_Group_preserves_epi : (forget Group).preserves_epimorphisms :=
+{ preserves := λ X Y f e, by rwa [epi_iff_surjective, ←category_theory.epi_iff_surjective] at e }
+
+end Group
+
 namespace CommGroup
 variables {A B : CommGroup.{u}} (f : A ⟶ B)
 
@@ -353,8 +366,12 @@ lemma epi_iff_surjective : epi f ↔ function.surjective f :=
 by rw [epi_iff_range_eq_top, monoid_hom.range_top_iff_surjective]
 
 @[to_additive]
-instance : functor.preserves_epimorphisms (forget₂ CommGroup Group) :=
-{ preserves := λ X Y f e, by rwa [epi_iff_surjective, ←@Group.epi_iff_surjective ⟨X⟩ ⟨Y⟩ f] at e }
+instance forget_CommGroup_preserves_mono : (forget CommGroup).preserves_monomorphisms :=
+{ preserves := λ X Y f e, by rwa [mono_iff_injective, ←category_theory.mono_iff_injective] at e }
+
+@[to_additive]
+instance forget_CommGroup_preserves_epi : (forget CommGroup).preserves_epimorphisms :=
+{ preserves := λ X Y f e, by rwa [epi_iff_surjective, ←category_theory.epi_iff_surjective] at e }
 
 end CommGroup
 

src/algebra/category/Module/epi_mono.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import linear_algebra.quotient
-import category_theory.epi_mono
+import algebra.category.Group.epi_mono
 import algebra.category.Module.basic
 
 /-!
@@ -55,4 +55,12 @@ instance mono_as_hom'_subtype (U : submodule R X) : mono ↾U.subtype :=
 instance epi_as_hom''_mkq (U : submodule R X) : epi ↿U.mkq :=
 (epi_iff_range_eq_top _).mpr $ submodule.range_mkq _
 
+instance forget_preserves_epimorphisms : (forget (Module.{v} R)).preserves_epimorphisms :=
+{ preserves := λ X Y f hf, by rwa [forget_map_eq_coe, category_theory.epi_iff_surjective,
+    ← epi_iff_surjective] }
+
+instance forget_preserves_monomorphisms : (forget (Module.{v} R)).preserves_monomorphisms :=
+{ preserves := λ X Y f hf, by rwa [forget_map_eq_coe, category_theory.mono_iff_injective,
+    ← mono_iff_injective] }
+
 end Module

src/category_theory/concrete_category/basic.lean

@@ -155,10 +155,24 @@ class has_forget₂ (C : Type v) (D : Type v') [category C] [concrete_category.{
   [concrete_category D] [has_forget₂ C D] : C ⥤ D :=
 has_forget₂.forget₂
 
-instance forget_faithful (C : Type v) (D : Type v') [category C] [concrete_category C] [category D]
+instance forget₂_faithful (C : Type v) (D : Type v') [category C] [concrete_category C] [category D]
   [concrete_category D] [has_forget₂ C D] : faithful (forget₂ C D) :=
 has_forget₂.forget_comp.faithful_of_comp
 
+instance forget₂_preserves_monomorphisms (C : Type v) (D : Type v') [category C]
+  [concrete_category C] [category D] [concrete_category D] [has_forget₂ C D]
+  [(forget C).preserves_monomorphisms] : (forget₂ C D).preserves_monomorphisms :=
+have (forget₂ C D ⋙ forget D).preserves_monomorphisms,
+  by { simp only [has_forget₂.forget_comp], apply_instance },
+by exactI functor.preserves_monomorphisms_of_preserves_of_reflects _ (forget D)
+
+instance forget₂_preserves_epimorphisms (C : Type v) (D : Type v') [category C]
+  [concrete_category C] [category D] [concrete_category D] [has_forget₂ C D]
+  [(forget C).preserves_epimorphisms] : (forget₂ C D).preserves_epimorphisms :=
+have (forget₂ C D ⋙ forget D).preserves_epimorphisms,
+  by { simp only [has_forget₂.forget_comp], apply_instance },
+by exactI functor.preserves_epimorphisms_of_preserves_of_reflects _ (forget D)
+
 instance induced_category.concrete_category {C : Type v} {D : Type v'} [category D]
   [concrete_category D] (f : C → D) :
   concrete_category (induced_category D f) :=
@@ -191,7 +205,9 @@ has_forget₂ C D :=
 { forget₂ := faithful.div _ _ _ @h_obj _ @h_map,
   forget_comp := by apply faithful.div_comp }
 
-instance has_forget_to_Type (C : Type v) [category C] [concrete_category C] :
+/-- Every forgetful functor factors through the identity functor. This is not a global instance as
+    it is prone to creating type class resolution loops. -/
+def has_forget_to_Type (C : Type v) [category C] [concrete_category C] :
   has_forget₂ C (Type u) :=
 { forget₂ := forget C,
   forget_comp := functor.comp_id _ }

src/category_theory/functor/epi_mono.lean

@@ -70,6 +70,22 @@ instance reflects_epimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [reflects_epimor
   [reflects_epimorphisms G] : reflects_epimorphisms (F ⋙ G) :=
 { reflects := λ X Y f h, (F.epi_of_epi_map (G.epi_of_epi_map h)) }
 
+lemma preserves_epimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+  [preserves_epimorphisms (F ⋙ G)] [reflects_epimorphisms G] : preserves_epimorphisms F :=
+⟨λ X Y f hf, G.epi_of_epi_map $ show epi ((F ⋙ G).map f), by exactI infer_instance⟩
+
+lemma preserves_monomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+  [preserves_monomorphisms (F ⋙ G)] [reflects_monomorphisms G] : preserves_monomorphisms F :=
+⟨λ X Y f hf, G.mono_of_mono_map $ show mono ((F ⋙ G).map f), by exactI infer_instance⟩
+
+lemma reflects_epimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+  [preserves_epimorphisms G] [reflects_epimorphisms (F ⋙ G)] : reflects_epimorphisms F :=
+⟨λ X Y f hf, (F ⋙ G).epi_of_epi_map $ show epi (G.map (F.map f)), by exactI infer_instance⟩
+
+lemma reflects_monomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
+  [preserves_monomorphisms G] [reflects_monomorphisms (F ⋙ G)] : reflects_monomorphisms F :=
+⟨λ X Y f hf, (F ⋙ G).mono_of_mono_map $ show mono (G.map (F.map f)), by exactI infer_instance⟩
+
 lemma preserves_monomorphisms.of_iso {F G : C ⥤ D} [preserves_monomorphisms F] (α : F ≅ G) :
   preserves_monomorphisms G :=
 { preserves := λ X Y f h,