refactor(Algebra/Module/Projective): generalize universes (#24697)

Generalize `(P : Type max u v)` to `(P : Type v) [Small.{v} R]` in [Module.Projective.of_lifting_property](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Projective.html#Module.Projective.of_lifting_property) and [IsProjective.iff_projective](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/Projective.html#IsProjective.iff_projective). Also generalize universes in [Module.Projective.iff_split](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Module/Projective.html#Module.Projective.iff_split).



Co-authored-by: Yongle Hu <140475041+mbkybky@users.noreply.github.com>
Co-authored-by: Thmoas-Guan <150537269+Thmoas-Guan@users.noreply.github.com>

Author: mbkybky

Mathlib/Algebra/Category/ModuleCat/Projective.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Kim Morrison
 -/
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
-import Mathlib.Algebra.Small.Group
 import Mathlib.Algebra.Module.Projective
+import Mathlib.Algebra.Small.Group
 import Mathlib.CategoryTheory.Preadditive.Projective.Basic
 
 /-!
@@ -14,36 +14,40 @@ import Mathlib.CategoryTheory.Preadditive.Projective.Basic
 
 universe v u w
 
-open CategoryTheory LinearMap ModuleCat
+open CategoryTheory ModuleCat
+
+variable {R : Type u} [Ring R] (P : ModuleCat.{v} R)
+
+instance ModuleCat.projective_of_categoryTheory_projective [Module.Projective R P] :
+    CategoryTheory.Projective P := by
+  refine ⟨fun E X epi => ?_⟩
+  obtain ⟨f, h⟩ := Module.projective_lifting_property X.hom E.hom
+    ((ModuleCat.epi_iff_surjective _).mp epi)
+  exact ⟨ofHom f, hom_ext h⟩
+
+instance ModuleCat.projective_of_module_projective [Small.{v} R] [Projective P] :
+    Module.Projective R P := by
+  refine Module.Projective.of_lifting_property ?_
+  intro _ _ _ _ _ _ f g s
+  have : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
+  exact ⟨(Projective.factorThru (↟g) (↟f)).hom,
+    ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩
 
 /-- The categorical notion of projective object agrees with the explicit module-theoretic notion. -/
-theorem IsProjective.iff_projective {R : Type u} [Ring R] {P : Type max u v} [AddCommGroup P]
-    [Module R P] : Module.Projective R P ↔ Projective (ModuleCat.of R P) := by
-  refine ⟨fun h => ?_, fun h => ?_⟩
-  · letI : Module.Projective R (ModuleCat.of R P) := h
-    refine ⟨fun E X epi => ?_⟩
-    obtain ⟨f, h⟩ := Module.projective_lifting_property X.hom E.hom
-      ((ModuleCat.epi_iff_surjective _).mp epi)
-    exact ⟨ofHom f, hom_ext h⟩
-  · refine Module.Projective.of_lifting_property.{u,v} ?_
-    intro E X mE mX sE sX f g s
-    haveI : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
-    letI : Projective (ModuleCat.of R P) := h
-    exact ⟨(Projective.factorThru (↟g) (↟f)).hom,
-      ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩
+theorem IsProjective.iff_projective [Small.{v} R] (P : Type v) [AddCommGroup P] [Module R P] :
+    Module.Projective R P ↔ Projective (of R P) :=
+  ⟨fun _ => (of R P).projective_of_categoryTheory_projective,
+    fun _ => (of R P).projective_of_module_projective⟩
 
 namespace ModuleCat
 
-variable {R : Type u} [Ring R] {M : ModuleCat.{v} R}
+variable {M : ModuleCat.{v} R}
 
 -- We transport the corresponding result from `Module.Projective`.
 /-- Modules that have a basis are projective. -/
-theorem projective_of_free {ι : Type w} (b : Basis ι R M) : Projective M := by
-  letI : Module.Projective R (ModuleCat.of R M) := Module.Projective.of_basis b
-  refine ⟨fun E X epi => ?_⟩
-  obtain ⟨f, h⟩ := Module.projective_lifting_property X.hom E.hom
-    ((ModuleCat.epi_iff_surjective _).mp epi)
-  exact ⟨ofHom f, hom_ext h⟩
+theorem projective_of_free {ι : Type w} (b : Basis ι R M) : Projective M :=
+  have : Module.Projective R M := Module.Projective.of_basis b
+  M.projective_of_categoryTheory_projective
 
 /-- The category of modules has enough projectives, since every module is a quotient of a free
   module. -/
@@ -54,7 +58,7 @@ instance enoughProjectives [Small.{v} R] : EnoughProjectives (ModuleCat.{v} R) w
       projective := projective_of_free e
       f := ofHom <| e.constr ℕ _root_.id
       epi := by
-        rw [epi_iff_range_eq_top, range_eq_top]
+        rw [epi_iff_range_eq_top, LinearMap.range_eq_top]
         refine fun m ↦ ⟨Finsupp.single m 1, ?_⟩
         simp [e, Basis.constr_apply] }⟩
 

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -343,6 +343,14 @@ theorem apply_symm_apply (c : M₂) : e (e.symm c) = c :=
 theorem symm_apply_apply (b : M) : e.symm (e b) = b :=
   e.left_inv b
 
+@[simp]
+theorem comp_symm : e.toLinearMap ∘ₛₗ e.symm.toLinearMap = LinearMap.id :=
+  LinearMap.ext e.apply_symm_apply
+
+@[simp]
+theorem symm_comp : e.symm.toLinearMap ∘ₛₗ e.toLinearMap= LinearMap.id :=
+  LinearMap.ext e.symm_apply_apply
+
 @[simp]
 theorem trans_symm : (e₁₂.trans e₂₃ : M₁ ≃ₛₗ[σ₁₃] M₃).symm = e₂₃.symm.trans e₁₂.symm :=
   rfl

Mathlib/Algebra/Module/Projective.lean

@@ -3,11 +3,9 @@ Copyright (c) 2021 Kevin Buzzard. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Antoine Labelle
 -/
-import Mathlib.Algebra.Module.Defs
-import Mathlib.LinearAlgebra.Finsupp.SumProd
-import Mathlib.LinearAlgebra.FreeModule.Basic
+import Mathlib.Algebra.Equiv.TransferInstance
 import Mathlib.LinearAlgebra.TensorProduct.Basis
-import Mathlib.LinearAlgebra.TensorProduct.Tower
+import Mathlib.Logic.UnivLE
 
 /-!
 
@@ -61,7 +59,7 @@ projective module
 
 -/
 
-universe u v
+universe w v u
 
 open LinearMap hiding id
 open Finsupp
@@ -205,12 +203,26 @@ variable {R : Type u} [Semiring R] {P : Type v} [AddCommMonoid P] [Module R P]
 variable {R₀ M N} [CommSemiring R₀] [Algebra R₀ R] [AddCommMonoid M] [Module R₀ M] [Module R M]
 variable [IsScalarTower R₀ R M] [AddCommMonoid N] [Module R₀ N]
 
+/-- A variant of `Projective.iff_split` allowing for a more flexible selection of the universe
+  for the free module `M`. -/
+theorem Projective.iff_split' [Small.{w} R] [Small.{w} P] : Module.Projective R P ↔
+    ∃ (M : Type w) (_ : AddCommMonoid M) (_ : Module R M) (_ : Module.Free R M)
+      (i : P →ₗ[R] M) (s : M →ₗ[R] P), s.comp i = LinearMap.id := by
+  let e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
+    Finsupp.mapDomain.linearEquiv _ R (equivShrink P).symm ≪≫ₗ
+      Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R)
+  refine ⟨fun ⟨i, hi⟩ ↦ ⟨(Shrink.{w} P) →₀ (Shrink.{w} R), _, _, Free.of_basis ⟨e⟩,
+    e.symm.toLinearMap ∘ₗ i, (linearCombination R id) ∘ₗ e.toLinearMap, ?_⟩,
+      fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
+  apply LinearMap.ext
+  simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, e.apply_symm_apply]
+  exact hi
+
 /-- A module is projective iff it is the direct summand of a free module. -/
 theorem Projective.iff_split : Module.Projective R P ↔
     ∃ (M : Type max u v) (_ : AddCommMonoid M) (_ : Module R M) (_ : Module.Free R M)
       (i : P →ₗ[R] M) (s : M →ₗ[R] P), s.comp i = LinearMap.id :=
-  ⟨fun ⟨i, hi⟩ ↦ ⟨P →₀ R, _, _, inferInstance, i, Finsupp.linearCombination R id, LinearMap.ext hi⟩,
-    fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
+  Projective.iff_split'.{max u v}
 
 open TensorProduct in
 instance Projective.tensorProduct [hM : Module.Projective R M] [hN : Module.Projective R₀ N] :
@@ -230,34 +242,36 @@ instance Projective.tensorProduct [hM : Module.Projective R M] [hN : Module.Proj
 
 end Ring
 
---This is in a different section because special universe restrictions are required.
 section OfLiftingProperty
 
--- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: generalize to `P : Type v`?
-/-- A module which satisfies the universal property is projective. Note that the universe variables
-in `huniv` are somewhat restricted. -/
-theorem Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type max u v}
-    [AddCommMonoid P] [Module R P]
+/-- A module which satisfies the universal property is projective. -/
+theorem Projective.of_lifting_property' {R : Type u} [Semiring R] {P : Type v}
+    [AddCommMonoid P] [Module R P] [Small.{v} R]
     -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
-    (huniv : ∀ {M : Type max v u} {N : Type max u v} [AddCommMonoid M] [AddCommMonoid N]
+    (h : ∀ {M : Type v} {N : Type v} [AddCommMonoid M] [AddCommMonoid N]
       [Module R M] [Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N),
         Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) :
     -- then `P` is projective.
-    Projective R P :=
-  .of_lifting_property'' (huniv · _)
+    Projective R P := by
+  refine of_lifting_property'' (fun p hp ↦ ?_)
+  let e := Finsupp.mapRange.linearEquiv (α := P) (Shrink.linearEquiv R R)
+  rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩
+  exact ⟨e.toLinearMap ∘ₗ g, hg⟩
 
--- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: generalize to `P : Type v`?
 /-- A variant of `of_lifting_property'` when we're working over a `[Ring R]`,
-which only requires quantifying over modules with an `AddCommGroup` instance. -/
-theorem Projective.of_lifting_property {R : Type u} [Ring R] {P : Type max u v} [AddCommGroup P]
-    [Module R P]
+  which only requires quantifying over modules with an `AddCommGroup` instance. -/
+theorem Projective.of_lifting_property {R : Type u} [Ring R] {P : Type v} [AddCommGroup P]
+    [Module R P] [Small.{v} R]
     -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
-    (huniv : ∀ {M : Type max v u} {N : Type max u v} [AddCommGroup M] [AddCommGroup N]
+    (h : ∀ {M : Type v} {N : Type v} [AddCommGroup M] [AddCommGroup N]
       [Module R M] [Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N),
         Function.Surjective f → ∃ h : P →ₗ[R] M, f.comp h = g) :
     -- then `P` is projective.
-    Projective R P :=
-  .of_lifting_property'' (huniv · _)
+    Projective R P := by
+  refine of_lifting_property'' (fun p hp ↦ ?_)
+  let e := Finsupp.mapRange.linearEquiv (α := P) (Shrink.linearEquiv R R)
+  rcases h (p ∘ₗ e.toLinearMap) LinearMap.id (hp.comp e.surjective) with ⟨g, hg⟩
+  exact ⟨e.toLinearMap ∘ₗ g, hg⟩
 
 end OfLiftingProperty
 

Mathlib/LinearAlgebra/Finsupp/Defs.lean

@@ -155,6 +155,15 @@ theorem lmapDomain_comp (f : α → α') (g : α' → α'') :
     lmapDomain M R (g ∘ f) = (lmapDomain M R g).comp (lmapDomain M R f) :=
   LinearMap.ext fun _ => mapDomain_comp
 
+/-- `Finsupp.mapDomain` as a `LinearEquiv`. -/
+def mapDomain.linearEquiv (f : α ≃ α') : (α →₀ M) ≃ₗ[R] (α' →₀ M) where
+  __ := lmapDomain M R f.toFun
+  invFun := mapDomain f.symm
+  left_inv _ := by
+    simp [← mapDomain_comp]
+  right_inv _ := by
+    simp [← mapDomain_comp]
+
 end LMapDomain
 
 section LComapDomain