feat(Algebra/Category): symmetric monoidal structure on SemimoduleCat (#30638)

+ Construct the symmetric monoidal structure on SemimoduleCat, and transport it to the same structure on ModuleCat (in a way preserving pre-existing defeqs) using the equivalence `ModuleCat.equivalenceSemimoduleCat` between the categories. Just a few proofs in the Representation library need to be fixed (in a straightforward way). Public API for ModuleCat is duplicated to SemimoduleCat.

Author: alreadydone

Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

@@ -6,6 +6,7 @@ Authors: Kevin Buzzard, Kim Morrison, Jakob von Raumer
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.LinearAlgebra.TensorProduct.Associator
 import Mathlib.CategoryTheory.Monoidal.Linear
+import Mathlib.CategoryTheory.Monoidal.Transport
 
 /-!
 # The monoidal category structure on R-modules
@@ -31,9 +32,9 @@ universe v w x u
 
 open CategoryTheory
 
-namespace ModuleCat
+namespace SemimoduleCat
 
-variable {R : Type u} [CommRing R]
+variable {R : Type u} [CommSemiring R]
 
 namespace MonoidalCategory
 
@@ -45,34 +46,34 @@ open TensorProduct
 attribute [local ext] TensorProduct.ext
 
 /-- (implementation) tensor product of R-modules -/
-def tensorObj (M N : ModuleCat R) : ModuleCat R :=
-  ModuleCat.of R (M ⊗[R] N)
+def tensorObj (M N : SemimoduleCat R) : SemimoduleCat R :=
+  SemimoduleCat.of R (M ⊗[R] N)
 
 /-- (implementation) tensor product of morphisms R-modules -/
-def tensorHom {M N M' N' : ModuleCat R} (f : M ⟶ N) (g : M' ⟶ N') :
+def tensorHom {M N M' N' : SemimoduleCat R} (f : M ⟶ N) (g : M' ⟶ N') :
     tensorObj M M' ⟶ tensorObj N N' :=
   ofHom <| TensorProduct.map f.hom g.hom
 
 /-- (implementation) left whiskering for R-modules -/
-def whiskerLeft (M : ModuleCat R) {N₁ N₂ : ModuleCat R} (f : N₁ ⟶ N₂) :
+def whiskerLeft (M : SemimoduleCat R) {N₁ N₂ : SemimoduleCat R} (f : N₁ ⟶ N₂) :
     tensorObj M N₁ ⟶ tensorObj M N₂ :=
   ofHom <| f.hom.lTensor M
 
 /-- (implementation) right whiskering for R-modules -/
-def whiskerRight {M₁ M₂ : ModuleCat R} (f : M₁ ⟶ M₂) (N : ModuleCat R) :
+def whiskerRight {M₁ M₂ : SemimoduleCat R} (f : M₁ ⟶ M₂) (N : SemimoduleCat R) :
     tensorObj M₁ N ⟶ tensorObj M₂ N :=
   ofHom <| f.hom.rTensor N
 
-theorem id_tensorHom_id (M N : ModuleCat R) :
-    tensorHom (𝟙 M) (𝟙 N) = 𝟙 (ModuleCat.of R (M ⊗ N)) := by
+theorem id_tensorHom_id (M N : SemimoduleCat R) :
+    tensorHom (𝟙 M) (𝟙 N) = 𝟙 (SemimoduleCat.of R (M ⊗ N)) := by
   ext : 1
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): even with high priority `ext` fails to find this.
   apply TensorProduct.ext
   rfl
 
 @[deprecated (since := "2025-07-14")] alias tensor_id := id_tensorHom_id
 
-theorem tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
+theorem tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
     (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
     tensorHom f₁ f₂ ≫ tensorHom g₁ g₂ = tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) := by
   ext : 1
@@ -81,30 +82,30 @@ theorem tensorHom_comp_tensorHom {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : ModuleCat R} (
   rfl
 
 /-- (implementation) the associator for R-modules -/
-def associator (M : ModuleCat.{v} R) (N : ModuleCat.{w} R) (K : ModuleCat.{x} R) :
+def associator (M : SemimoduleCat.{v} R) (N : SemimoduleCat.{w} R) (K : SemimoduleCat.{x} R) :
     tensorObj (tensorObj M N) K ≅ tensorObj M (tensorObj N K) :=
-  (TensorProduct.assoc R M N K).toModuleIso
+  (TensorProduct.assoc R M N K).toModuleIsoₛ
 
 /-- (implementation) the left unitor for R-modules -/
-def leftUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (R ⊗[R] M) ≅ M :=
-  (TensorProduct.lid R M).toModuleIso
+def leftUnitor (M : SemimoduleCat.{u} R) : SemimoduleCat.of R (R ⊗[R] M) ≅ M :=
+  (TensorProduct.lid R M).toModuleIsoₛ
 
 /-- (implementation) the right unitor for R-modules -/
-def rightUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (M ⊗[R] R) ≅ M :=
-  (TensorProduct.rid R M).toModuleIso
+def rightUnitor (M : SemimoduleCat.{u} R) : SemimoduleCat.of R (M ⊗[R] R) ≅ M :=
+  (TensorProduct.rid R M).toModuleIsoₛ
 
 @[simps -isSimp]
-instance instMonoidalCategoryStruct : MonoidalCategoryStruct (ModuleCat.{u} R) where
+instance instMonoidalCategoryStruct : MonoidalCategoryStruct (SemimoduleCat.{u} R) where
   tensorObj := tensorObj
   whiskerLeft := whiskerLeft
   whiskerRight := whiskerRight
-  tensorHom f g := ofHom <| TensorProduct.map f.hom g.hom
-  tensorUnit := ModuleCat.of R R
+  tensorHom := tensorHom
+  tensorUnit := SemimoduleCat.of R R
   associator := associator
   leftUnitor := leftUnitor
   rightUnitor := rightUnitor
 
-theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
+theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : SemimoduleCat R} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂)
     (f₃ : X₃ ⟶ Y₃) :
     tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
       (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃) := by
@@ -113,7 +114,7 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f
   intro x y z
   rfl
 
-theorem pentagon (W X Y Z : ModuleCat R) :
+theorem pentagon (W X Y Z : SemimoduleCat R) :
     whiskerRight (associator W X Y).hom Z ≫
         (associator W (tensorObj X Y) Z).hom ≫ whiskerLeft W (associator X Y Z).hom =
       (associator (tensorObj W X) Y Z).hom ≫ (associator W X (tensorObj Y Z)).hom := by
@@ -122,8 +123,8 @@ theorem pentagon (W X Y Z : ModuleCat R) :
   intro w x y z
   rfl
 
-theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
-    tensorHom (𝟙 (ModuleCat.of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f := by
+theorem leftUnitor_naturality {M N : SemimoduleCat R} (f : M ⟶ N) :
+    tensorHom (𝟙 (SemimoduleCat.of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f := by
   ext : 1
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
   apply TensorProduct.ext
@@ -133,8 +134,8 @@ theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
   rw [LinearMap.map_smul]
   rfl
 
-theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
-    tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f := by
+theorem rightUnitor_naturality {M N : SemimoduleCat R} (f : M ⟶ N) :
+    tensorHom f (𝟙 (SemimoduleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f := by
   ext : 1
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): broken ext
   apply TensorProduct.ext
@@ -144,8 +145,8 @@ theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
   rw [LinearMap.map_smul]
   rfl
 
-theorem triangle (M N : ModuleCat.{u} R) :
-    (associator M (ModuleCat.of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom =
+theorem triangle (M N : SemimoduleCat.{u} R) :
+    (associator M (SemimoduleCat.of R R) N).hom ≫ tensorHom (𝟙 M) (leftUnitor N).hom =
       tensorHom (rightUnitor M).hom (𝟙 N) := by
   ext : 1
   apply TensorProduct.ext_threefold
@@ -156,7 +157,7 @@ end MonoidalCategory
 
 open MonoidalCategory
 
-instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCategory.ofTensorHom
+instance monoidalCategory : MonoidalCategory (SemimoduleCat.{u} R) := MonoidalCategory.ofTensorHom
   (id_tensorHom_id := fun M N ↦ id_tensorHom_id M N)
   (tensorHom_comp_tensorHom := fun f g h ↦ MonoidalCategory.tensorHom_comp_tensorHom f g h)
   (associator_naturality := fun f g h ↦ MonoidalCategory.associator_naturality f g h)
@@ -165,6 +166,161 @@ instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCatego
   (pentagon := fun M N K L ↦ pentagon M N K L)
   (triangle := fun M N ↦ triangle M N)
 
+/-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative semiring. -/
+instance : CommSemiring ((𝟙_ (SemimoduleCat.{u} R) : SemimoduleCat.{u} R) : Type u) :=
+  inferInstanceAs <| CommSemiring R
+
+theorem hom_tensorHom {K L M N : SemimoduleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) :
+    (f ⊗ₘ g).hom = TensorProduct.map f.hom g.hom :=
+  rfl
+
+theorem hom_whiskerLeft (L : SemimoduleCat.{u} R) {M N : SemimoduleCat.{u} R} (f : M ⟶ N) :
+    (L ◁ f).hom = f.hom.lTensor L :=
+  rfl
+
+theorem hom_whiskerRight {L M : SemimoduleCat.{u} R} (f : L ⟶ M) (N : SemimoduleCat.{u} R) :
+    (f ▷ N).hom = f.hom.rTensor N :=
+  rfl
+
+theorem hom_hom_leftUnitor {M : SemimoduleCat.{u} R} :
+    (λ_ M).hom.hom = (TensorProduct.lid _ _).toLinearMap :=
+  rfl
+
+theorem hom_inv_leftUnitor {M : SemimoduleCat.{u} R} :
+    (λ_ M).inv.hom = (TensorProduct.lid _ _).symm.toLinearMap :=
+  rfl
+
+theorem hom_hom_rightUnitor {M : SemimoduleCat.{u} R} :
+    (ρ_ M).hom.hom = (TensorProduct.rid _ _).toLinearMap :=
+  rfl
+
+theorem hom_inv_rightUnitor {M : SemimoduleCat.{u} R} :
+    (ρ_ M).inv.hom = (TensorProduct.rid _ _).symm.toLinearMap :=
+  rfl
+
+theorem hom_hom_associator {M N K : SemimoduleCat.{u} R} :
+    (α_ M N K).hom.hom = (TensorProduct.assoc _ _ _ _).toLinearMap :=
+  rfl
+
+theorem hom_inv_associator {M N K : SemimoduleCat.{u} R} :
+    (α_ M N K).inv.hom = (TensorProduct.assoc _ _ _ _).symm.toLinearMap :=
+  rfl
+
+namespace MonoidalCategory
+
+@[simp]
+theorem tensorHom_tmul {K L M N : SemimoduleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K) (m : M) :
+    (f ⊗ₘ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=
+  rfl
+
+@[simp]
+theorem whiskerLeft_apply (L : SemimoduleCat.{u} R) {M N : SemimoduleCat.{u} R} (f : M ⟶ N)
+    (l : L) (m : M) :
+    (L ◁ f) (l ⊗ₜ m) = l ⊗ₜ f m :=
+  rfl
+
+@[simp]
+theorem whiskerRight_apply {L M : SemimoduleCat.{u} R} (f : L ⟶ M) (N : SemimoduleCat.{u} R)
+    (l : L) (n : N) :
+    (f ▷ N) (l ⊗ₜ n) = f l ⊗ₜ n :=
+  rfl
+
+@[simp]
+theorem leftUnitor_hom_apply {M : SemimoduleCat.{u} R} (r : R) (m : M) :
+    ((λ_ M).hom : 𝟙_ (SemimoduleCat R) ⊗ M ⟶ M) (r ⊗ₜ[R] m) = r • m :=
+  TensorProduct.lid_tmul m r
+
+@[simp]
+theorem leftUnitor_inv_apply {M : SemimoduleCat.{u} R} (m : M) :
+    ((λ_ M).inv : M ⟶ 𝟙_ (SemimoduleCat.{u} R) ⊗ M) m = 1 ⊗ₜ[R] m :=
+  TensorProduct.lid_symm_apply m
+
+@[simp]
+theorem rightUnitor_hom_apply {M : SemimoduleCat.{u} R} (m : M) (r : R) :
+    ((ρ_ M).hom : M ⊗ 𝟙_ (SemimoduleCat R) ⟶ M) (m ⊗ₜ r) = r • m :=
+  TensorProduct.rid_tmul m r
+
+@[simp]
+theorem rightUnitor_inv_apply {M : SemimoduleCat.{u} R} (m : M) :
+    ((ρ_ M).inv : M ⟶ M ⊗ 𝟙_ (SemimoduleCat.{u} R)) m = m ⊗ₜ[R] 1 :=
+  TensorProduct.rid_symm_apply m
+
+@[simp]
+theorem associator_hom_apply {M N K : SemimoduleCat.{u} R} (m : M) (n : N) (k : K) :
+    ((α_ M N K).hom : (M ⊗ N) ⊗ K ⟶ M ⊗ N ⊗ K) (m ⊗ₜ n ⊗ₜ k) = m ⊗ₜ (n ⊗ₜ k) :=
+  rfl
+
+@[simp]
+theorem associator_inv_apply {M N K : SemimoduleCat.{u} R} (m : M) (n : N) (k : K) :
+    ((α_ M N K).inv : M ⊗ N ⊗ K ⟶ (M ⊗ N) ⊗ K) (m ⊗ₜ (n ⊗ₜ k)) = m ⊗ₜ n ⊗ₜ k :=
+  rfl
+
+variable {M₁ M₂ M₃ M₄ : SemimoduleCat.{u} R}
+
+section
+
+variable (f : M₁ → M₂ → M₃) (h₁ : ∀ m₁ m₂ n, f (m₁ + m₂) n = f m₁ n + f m₂ n)
+  (h₂ : ∀ (a : R) m n, f (a • m) n = a • f m n)
+  (h₃ : ∀ m n₁ n₂, f m (n₁ + n₂) = f m n₁ + f m n₂)
+  (h₄ : ∀ (a : R) m n, f m (a • n) = a • f m n)
+
+/-- Construct for morphisms from the tensor product of two objects in `SemimoduleCat`. -/
+def tensorLift : M₁ ⊗ M₂ ⟶ M₃ :=
+  ofHom <| TensorProduct.lift (LinearMap.mk₂ R f h₁ h₂ h₃ h₄)
+
+@[simp]
+lemma tensorLift_tmul (m : M₁) (n : M₂) :
+    tensorLift f h₁ h₂ h₃ h₄ (m ⊗ₜ n) = f m n := rfl
+
+end
+
+lemma tensor_ext {f g : M₁ ⊗ M₂ ⟶ M₃} (h : ∀ m n, f.hom (m ⊗ₜ n) = g.hom (m ⊗ₜ n)) :
+    f = g :=
+  hom_ext <| TensorProduct.ext (by ext; apply h)
+
+/-- Extensionality lemma for morphisms from a module of the form `(M₁ ⊗ M₂) ⊗ M₃`. -/
+lemma tensor_ext₃' {f g : (M₁ ⊗ M₂) ⊗ M₃ ⟶ M₄}
+    (h : ∀ m₁ m₂ m₃, f (m₁ ⊗ₜ m₂ ⊗ₜ m₃) = g (m₁ ⊗ₜ m₂ ⊗ₜ m₃)) :
+    f = g :=
+  hom_ext <| TensorProduct.ext_threefold h
+
+/-- Extensionality lemma for morphisms from a module of the form `M₁ ⊗ (M₂ ⊗ M₃)`. -/
+lemma tensor_ext₃ {f g : M₁ ⊗ (M₂ ⊗ M₃) ⟶ M₄}
+    (h : ∀ m₁ m₂ m₃, f (m₁ ⊗ₜ (m₂ ⊗ₜ m₃)) = g (m₁ ⊗ₜ (m₂ ⊗ₜ m₃))) :
+    f = g := by
+  rw [← cancel_epi (α_ _ _ _).hom]
+  exact tensor_ext₃' h
+
+end MonoidalCategory
+
+end SemimoduleCat
+
+namespace ModuleCat
+
+variable {R : Type u} [CommRing R]
+
+@[simps -isSimp]
+instance MonoidalCategory.instMonoidalCategoryStruct :
+    MonoidalCategoryStruct (ModuleCat.{u} R) where
+  tensorObj M N := of R (TensorProduct R M N)
+  whiskerLeft M _ _ f := ofHom <| f.hom.lTensor M
+  whiskerRight f M := ofHom <| f.hom.rTensor M
+  tensorHom f g := ofHom <| TensorProduct.map f.hom g.hom
+  tensorUnit := of R R
+  associator M N K := (TensorProduct.assoc R M N K).toModuleIso
+  leftUnitor M := (TensorProduct.lid R M).toModuleIso
+  rightUnitor M := (TensorProduct.rid R M).toModuleIso
+
+instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) :=
+  Monoidal.induced equivalenceSemimoduleCat.functor
+  { μIso _ _ := .refl _
+    εIso := .refl _
+    associator_eq _ _ _ := by ext1; exact TensorProduct.ext (TensorProduct.ext rfl)
+    leftUnitor_eq _ := by ext1; exact TensorProduct.ext rfl
+    rightUnitor_eq _ := by ext1; exact TensorProduct.ext rfl }
+
+open MonoidalCategory
+
 /-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative ring. -/
 instance : CommRing ((𝟙_ (ModuleCat.{u} R) : ModuleCat.{u} R) : Type u) :=
   inferInstanceAs <| CommRing R