feat: category of $R$-modules has enough injectives (#7392)

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

Mathlib.lean

@@ -70,6 +70,7 @@ import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
 import Mathlib.Algebra.Category.ModuleCat.Free
 import Mathlib.Algebra.Category.ModuleCat.Images
+import Mathlib.Algebra.Category.ModuleCat.Injective
 import Mathlib.Algebra.Category.ModuleCat.Kernels
 import Mathlib.Algebra.Category.ModuleCat.Limits
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -3,7 +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
 -/
-import Mathlib.Algebra.Category.ModuleCat.Basic
+import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.RingTheory.TensorProduct
 
 #align_import algebra.category.Module.change_of_rings from "leanprover-community/mathlib"@"56b71f0b55c03f70332b862e65c3aa1aa1249ca1"
@@ -84,11 +84,15 @@ def restrictScalars {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →
   map_comp _ _ := LinearMap.ext fun _ => rfl
 #align category_theory.Module.restrict_scalars ModuleCat.restrictScalars
 
-instance {R : Type u₁} {S : Type u₂} [CommRing R] [CommRing S] (f : R →+* S) :
+instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
     CategoryTheory.Faithful (restrictScalars.{v} f) where
   map_injective h :=
     LinearMap.ext fun x => by simpa only using FunLike.congr_fun h x
 
+instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] (f : R →+* S) :
+    (restrictScalars.{v} f).PreservesMonomorphisms where
+  preserves _ h := by rwa [mono_iff_injective] at h ⊢
+
 -- Porting note: this should be automatic
 instance {R : Type u₁} {S : Type u₂} [Ring R] [Ring S] {f : R →+* S}
     {M : ModuleCat.{v} S} : Module R <| (restrictScalars f).obj M :=

Mathlib/Algebra/Category/ModuleCat/Injective.lean

@@ -0,0 +1,33 @@
+/-
+Copyright (c) 2023 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import Mathlib.Algebra.Category.ModuleCat.Abelian
+import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
+import Mathlib.Algebra.Category.GroupCat.Abelian
+import Mathlib.Algebra.Category.GroupCat.Injective
+import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
+
+/-!
+# Category of $R$-modules has enough injectives
+
+we lift enough injectives of abelian groups to arbitrary $R$-modules by adjoint functors
+`restrictScalars ⊣ coextendScalars`
+
+## Implementation notes
+This file is not part of `Algebra/Module/Injective.lean` to prevent import loop: enough-injectives
+of abelian groups needs `Algebra/Module/Injective.lean` and this file needs enough-injectives of
+abelian groups.
+-/
+
+open CategoryTheory
+
+universe u v
+variable (R : Type u) [Ring R]
+
+instance : EnoughInjectives (ModuleCat.{v} ℤ) :=
+  EnoughInjectives.of_equivalence (forget₂ (ModuleCat ℤ) AddCommGroupCat)
+
+lemma ModuleCat.enoughInjectives : EnoughInjectives (ModuleCat.{max v u} R) :=
+  EnoughInjectives.of_adjunction (ModuleCat.restrictCoextendScalarsAdj.{max v u} (algebraMap ℤ R))

Mathlib/CategoryTheory/Functor/EpiMono.lean

@@ -321,6 +321,12 @@ instance strongEpi_map_of_isEquivalence [IsEquivalence F] (f : A ⟶ B) [_h : St
   F.asEquivalence.toAdjunction.strongEpi_map_of_strongEpi f
 #align category_theory.adjunction.strong_epi_map_of_is_equivalence CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence
 
+instance (adj : F ⊣ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) [hf : Mono f] [F.ReflectsMonomorphisms] :
+    Mono (adj.homEquiv _ _ f) :=
+  F.mono_of_mono_map <| by
+    rw [← (homEquiv adj X Y).symm_apply_apply f] at hf
+    exact mono_of_mono_fac adj.homEquiv_counit.symm
+
 end CategoryTheory.Adjunction
 
 namespace CategoryTheory.Functor

Mathlib/CategoryTheory/Preadditive/Injective.lean

@@ -346,8 +346,35 @@ def mapInjectivePresentation (adj : F ⊣ G) [F.PreservesMonomorphisms] (X : D)
     haveI : PreservesLimitsOfSize.{0, 0} G := adj.rightAdjointPreservesLimits; infer_instance
 #align category_theory.adjunction.map_injective_presentation CategoryTheory.Adjunction.mapInjectivePresentation
 
+/-- Given an adjunction `F ⊣ G` such that `F` preserves monomorphisms and is faithful,
+  then any injective presentation of `F(X)` can be pulled back to an injective presentation of `X`.
+  This is similar to `mapInjectivePresentation`. -/
+def injectivePresentationOfMap (adj : F ⊣ G)
+    [F.PreservesMonomorphisms] [F.ReflectsMonomorphisms] (X : C)
+    (I : InjectivePresentation <| F.obj X) :
+    InjectivePresentation X where
+  J := G.obj I.J
+  injective := Injective.injective_of_adjoint adj _
+  f := adj.homEquiv _ _ I.f
+
 end Adjunction
 
+/--
+[Lemma 3.8](https://ncatlab.org/nlab/show/injective+object#preservation_of_injective_objects)
+-/
+lemma EnoughInjectives.of_adjunction {C : Type u₁} {D : Type u₂}
+    [Category.{v₁} C] [Category.{v₂} D]
+    {L : C ⥤ D} {R : D ⥤ C} (adj : L ⊣ R) [L.PreservesMonomorphisms] [L.ReflectsMonomorphisms]
+    [EnoughInjectives D] : EnoughInjectives C where
+  presentation _ :=
+    ⟨adj.injectivePresentationOfMap _ (EnoughInjectives.presentation _).some⟩
+
+/-- An equivalence of categories transfers enough injectives. -/
+lemma EnoughInjectives.of_equivalence {C : Type u₁} {D : Type u₂}
+    [Category.{v₁} C] [Category.{v₂} D]
+    (e : C ⥤ D) [IsEquivalence e] [EnoughInjectives D] : EnoughInjectives C :=
+  EnoughInjectives.of_adjunction (adj := e.asEquivalence.toAdjunction)
+
 namespace Equivalence
 
 variable {D : Type*} [Category D] (F : C ≌ D)
@@ -358,22 +385,12 @@ theorem map_injective_iff (P : C) : Injective (F.functor.obj P) ↔ Injective P
 /-- Given an equivalence of categories `F`, an injective presentation of `F(X)` induces an
 injective presentation of `X.` -/
 def injectivePresentationOfMapInjectivePresentation (X : C)
-    (I : InjectivePresentation (F.functor.obj X)) : InjectivePresentation X where
-  J := F.inverse.obj I.J
-  injective := Adjunction.map_injective F.toAdjunction I.J I.injective
-  f := F.unit.app _ ≫ F.inverse.map I.f
-  mono := mono_comp _ _
+    (I : InjectivePresentation (F.functor.obj X)) : InjectivePresentation X :=
+  F.toAdjunction.injectivePresentationOfMap _ I
 #align category_theory.equivalence.injective_presentation_of_map_injective_presentation CategoryTheory.Equivalence.injectivePresentationOfMapInjectivePresentation
 
-theorem enoughInjectives_iff (F : C ≌ D) : EnoughInjectives C ↔ EnoughInjectives D := by
-  constructor
-  all_goals intro H; constructor; intro X; constructor
-  · exact
-      F.symm.injectivePresentationOfMapInjectivePresentation _
-        (Nonempty.some (H.presentation (F.inverse.obj X)))
-  · exact
-      F.injectivePresentationOfMapInjectivePresentation X
-        (Nonempty.some (H.presentation (F.functor.obj X)))
+theorem enoughInjectives_iff (F : C ≌ D) : EnoughInjectives C ↔ EnoughInjectives D :=
+  ⟨fun h => h.of_adjunction F.symm.toAdjunction, fun h => h.of_adjunction F.toAdjunction⟩
 #align category_theory.equivalence.enough_injectives_iff CategoryTheory.Equivalence.enoughInjectives_iff
 
 end Equivalence