chore: do not depend on CategoryTheory in Module.Injective (#17747)

The category-theoretic results can be split between `Mathlib/Algebra/Category/Grp/Injective.lean` and `Mathlib/Algebra/Category/ModuleCat/Injective.lean` instead, with no changes to downstream proofs.



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

Author: eric-wieser

Mathlib.lean

@@ -100,6 +100,7 @@ import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
 import Mathlib.Algebra.Category.ModuleCat.Colimits
 import Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
 import Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
+import Mathlib.Algebra.Category.ModuleCat.EnoughInjectives
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
 import Mathlib.Algebra.Category.ModuleCat.Free

Mathlib/Algebra/Category/Grp/EnoughInjectives.lean

@@ -7,6 +7,7 @@ Authors: Jujian Zhang, Junyan Xu
 import Mathlib.Algebra.Module.CharacterModule
 import Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
 import Mathlib.Algebra.Category.Grp.EpiMono
+import Mathlib.Algebra.Category.Grp.Injective
 
 /-!
 
@@ -17,8 +18,7 @@ injective presentation for `A`, hence category of abelian groups has enough inje
 
 ## Implementation notes
 
-This file is split from `Mathlib.Algebra.Grp.Injective` is to prevent import loop.
-This file's dependency imports `Mathlib.Algebra.Grp.Injective`.
+This file is split from `Mathlib.Algebra.Category.Grp.Injective` to prevent import loops.
 -/
 
 open CategoryTheory

Mathlib/Algebra/Category/Grp/Injective.lean

@@ -3,9 +3,11 @@ 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.EpiMono
 import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
 import Mathlib.Algebra.EuclideanDomain.Int
-import Mathlib.Algebra.Module.Injective
+import Mathlib.Algebra.Category.ModuleCat.Injective
+import Mathlib.CategoryTheory.Preadditive.Injective
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.Topology.Instances.AddCircle
 
@@ -40,7 +42,6 @@ universe u
 
 variable (A : Type u) [AddCommGroup A]
 
-
 theorem Module.Baer.of_divisible [DivisibleBy A ℤ] : Module.Baer ℤ A := fun I g ↦ by
   rcases IsPrincipalIdealRing.principal I with ⟨m, rfl⟩
   obtain rfl | h0 := eq_or_ne m 0

Mathlib/Algebra/Category/ModuleCat/EnoughInjectives.lean

@@ -0,0 +1,34 @@
+/-
+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.ChangeOfRings
+import Mathlib.Algebra.Category.ModuleCat.Injective
+import Mathlib.Algebra.Category.Grp.EnoughInjectives
+import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
+import Mathlib.Logic.Equiv.TransferInstance
+
+/-!
+# Category of $R$-modules has enough injectives
+
+we lift enough injectives of abelian groups to arbitrary $R$-modules by adjoint functors
+`restrictScalars ⊣ coextendScalars`
+-/
+
+open CategoryTheory
+
+universe v u
+variable (R : Type u) [Ring R]
+
+instance : EnoughInjectives (ModuleCat.{v} ℤ) :=
+  EnoughInjectives.of_equivalence (forget₂ (ModuleCat ℤ) AddCommGrp)
+
+lemma ModuleCat.enoughInjectives : EnoughInjectives (ModuleCat.{max v u} R) :=
+  EnoughInjectives.of_adjunction (ModuleCat.restrictCoextendScalarsAdj.{max v u} (algebraMap ℤ R))
+
+open ModuleCat in
+instance [UnivLE.{u,v}] : EnoughInjectives (ModuleCat.{v} R) :=
+  letI := (equivShrink.{v} R).symm.ring
+  letI := enoughInjectives.{v} (Shrink.{v} R)
+  EnoughInjectives.of_equivalence (restrictScalars (equivShrink R).symm.ringEquiv.toRingHom)

Mathlib/Algebra/Category/ModuleCat/Injective.lean

@@ -3,36 +3,47 @@ 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.ChangeOfRings
-import Mathlib.Algebra.Category.Grp.EnoughInjectives
-import Mathlib.Algebra.Category.Grp.ZModuleEquivalence
-import Mathlib.Logic.Equiv.TransferInstance
+import Mathlib.Algebra.Module.Injective
+import Mathlib.CategoryTheory.Preadditive.Injective
+import Mathlib.Algebra.Category.ModuleCat.EpiMono
 
 /-!
-# 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.
+# Injective objects in the category of $R$-modules
 -/
 
 open CategoryTheory
 
-universe v u
-variable (R : Type u) [Ring R]
-
-instance : EnoughInjectives (ModuleCat.{v} ℤ) :=
-  EnoughInjectives.of_equivalence (forget₂ (ModuleCat ℤ) AddCommGrp)
-
-lemma ModuleCat.enoughInjectives : EnoughInjectives (ModuleCat.{max v u} R) :=
-  EnoughInjectives.of_adjunction (ModuleCat.restrictCoextendScalarsAdj.{max v u} (algebraMap ℤ R))
-
-open ModuleCat in
-instance [UnivLE.{u,v}] : EnoughInjectives (ModuleCat.{v} R) :=
-  letI := (equivShrink.{v} R).symm.ring
-  letI := enoughInjectives.{v} (Shrink.{v} R)
-  EnoughInjectives.of_equivalence (restrictScalars (equivShrink R).symm.ringEquiv.toRingHom)
+universe u v
+variable (R : Type u) (M : Type v) [Ring R] [AddCommGroup M] [Module R M]
+namespace Module
+
+theorem injective_object_of_injective_module [inj : Injective R M] :
+    CategoryTheory.Injective (ModuleCat.of R M) where
+  factors g f m :=
+    have ⟨l, h⟩ := inj.out f ((ModuleCat.mono_iff_injective f).mp m) g
+    ⟨l, LinearMap.ext h⟩
+
+theorem injective_module_of_injective_object
+    [inj : CategoryTheory.Injective <| ModuleCat.of R M] :
+    Module.Injective R M where
+  out X Y _ _ _ _ f hf g := by
+    have : CategoryTheory.Mono (ModuleCat.asHom f) := (ModuleCat.mono_iff_injective _).mpr hf
+    obtain ⟨l, rfl⟩ := inj.factors (ModuleCat.asHom g) (ModuleCat.asHom f)
+    exact ⟨l, fun _ ↦ rfl⟩
+
+theorem injective_iff_injective_object :
+    Module.Injective R M ↔
+    CategoryTheory.Injective (ModuleCat.of R M) :=
+  ⟨fun _ => injective_object_of_injective_module R M,
+   fun _ => injective_module_of_injective_object R M⟩
+
+end Module
+
+
+instance ModuleCat.ulift_injective_of_injective.{v'}
+    [Small.{v} R] [AddCommGroup M] [Module R M]
+    [CategoryTheory.Injective <| ModuleCat.of R M] :
+    CategoryTheory.Injective <| ModuleCat.of R (ULift.{v'} M) :=
+  Module.injective_object_of_injective_module
+    (inj := Module.ulift_injective_of_injective
+      (inj := Module.injective_module_of_injective_object _ _))

Mathlib/Algebra/Module/Injective.lean

@@ -3,11 +3,10 @@ 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.CategoryTheory.Preadditive.Injective
-import Mathlib.Algebra.Category.ModuleCat.EpiMono
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.LinearAlgebra.LinearPMap
 import Mathlib.Logic.Equiv.TransferInstance
+import Mathlib.Logic.Small.Basic
 
 /-!
 # Injective modules
@@ -33,6 +32,7 @@ import Mathlib.Logic.Equiv.TransferInstance
 
 -/
 
+assert_not_exists ModuleCat
 
 noncomputable section
 
@@ -57,26 +57,6 @@ map to `Q`, i.e. in the following diagram, if `f` is injective then there is an
     (f : X →ₗ[R] Y) (_ : Function.Injective f) (g : X →ₗ[R] Q),
     ∃ h : Y →ₗ[R] Q, ∀ x, h (f x) = g x
 
-theorem Module.injective_object_of_injective_module [inj : Module.Injective R Q] :
-    CategoryTheory.Injective (ModuleCat.of R Q) where
-  factors g f m :=
-    have ⟨l, h⟩ := inj.out f ((ModuleCat.mono_iff_injective f).mp m) g
-    ⟨l, LinearMap.ext h⟩
-
-theorem Module.injective_module_of_injective_object
-    [inj : CategoryTheory.Injective <| ModuleCat.of R Q] :
-    Module.Injective R Q where
-  out X Y _ _ _ _ f hf g := by
-    have : CategoryTheory.Mono (ModuleCat.asHom f) := (ModuleCat.mono_iff_injective _).mpr hf
-    obtain ⟨l, rfl⟩ := inj.factors (ModuleCat.asHom g) (ModuleCat.asHom f)
-    exact ⟨l, fun _ ↦ rfl⟩
-
-theorem Module.injective_iff_injective_object :
-    Module.Injective R Q ↔
-    CategoryTheory.Injective (ModuleCat.of R Q) :=
-  ⟨fun _ => injective_object_of_injective_module R Q,
-   fun _ => injective_module_of_injective_object R Q⟩
-
 /-- An `R`-module `Q` satisfies Baer's criterion if any `R`-linear map from an `Ideal R` extends to
 an `R`-linear map `R ⟶ Q`-/
 def Module.Baer : Prop :=
@@ -440,13 +420,6 @@ lemma Module.injective_iff_ulift_injective :
   ⟨Module.ulift_injective_of_injective R,
    Module.injective_of_ulift_injective R⟩
 
-instance ModuleCat.ulift_injective_of_injective
-    [inj : CategoryTheory.Injective <| ModuleCat.of R M] :
-    CategoryTheory.Injective <| ModuleCat.of R (ULift.{v'} M) :=
-  Module.injective_object_of_injective_module
-    (inj := Module.ulift_injective_of_injective
-      (inj := Module.injective_module_of_injective_object (inj := inj)))
-
 end ULift
 
 section lifting_property