refactor: Move the data fields of MonoidalCategory into a Struct …

…class (#7279)

This matches the approach for `CategoryStruct`, and allows us to use the notation within `MonoidalCategory`.

It also makes it easier to induce the lawful structure along a faithful functor, as again it means by the time we are providing the proof fields, the notation is already available.

This also eliminates `tensorUnit` vs `tensorUnit'`, adding a custom pretty-printer to provide the unprimed version with appropriate notation.

Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

@@ -14,6 +14,7 @@ import Mathlib.RingTheory.TensorProduct
 -/
 
 open CategoryTheory
+open scoped MonoidalCategory
 
 universe v u
 
@@ -39,58 +40,49 @@ noncomputable abbrev tensorHom {W X Y Z : AlgebraCat.{u} R} (f : W ⟶ X) (g : Y
     tensorObj W Y ⟶ tensorObj X Z :=
   Algebra.TensorProduct.map f g
 
-/-- Auxiliary definition used to fight a timeout when building
-`AlgebraCat.instMonoidalCategory`. -/
-@[simps!]
-abbrev tensorUnit : AlgebraCat.{u} R := of R R
+open MonoidalCategory
 
-/-- Auxiliary definition used to fight a timeout when building
-`AlgebraCat.instMonoidalCategory`. -/
-noncomputable abbrev associator (X Y Z : AlgebraCat.{u} R) :
-    tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z) :=
-  (Algebra.TensorProduct.assoc R X Y Z).toAlgebraIso
+end instMonoidalCategory
 
-open MonoidalCategory
+open instMonoidalCategory
+
+instance : MonoidalCategoryStruct (AlgebraCat.{u} R) where
+  tensorObj := instMonoidalCategory.tensorObj
+  whiskerLeft X _ _ f := tensorHom (𝟙 X) f
+  whiskerRight {X₁ X₂} (f : X₁ ⟶ X₂) Y := tensorHom f (𝟙 Y)
+  tensorHom := tensorHom
+  tensorUnit := of R R
+  associator X Y Z := (Algebra.TensorProduct.assoc R X Y Z).toAlgebraIso
+  leftUnitor X := (Algebra.TensorProduct.lid R X).toAlgebraIso
+  rightUnitor X := (Algebra.TensorProduct.rid R R X).toAlgebraIso
 
 theorem forget₂_map_associator_hom (X Y Z : AlgebraCat.{u} R) :
-    (forget₂ (AlgebraCat R) (ModuleCat R)).map (associator X Y Z).hom =
+    (forget₂ (AlgebraCat R) (ModuleCat R)).map (α_ X Y Z).hom =
       (α_
         (forget₂ _ (ModuleCat R) |>.obj X)
         (forget₂ _ (ModuleCat R) |>.obj Y)
         (forget₂ _ (ModuleCat R) |>.obj Z)).hom := by
   rfl
 
 theorem forget₂_map_associator_inv (X Y Z : AlgebraCat.{u} R) :
-    (forget₂ (AlgebraCat R) (ModuleCat R)).map (associator X Y Z).inv =
+    (forget₂ (AlgebraCat R) (ModuleCat R)).map (α_ X Y Z).inv =
       (α_
         (forget₂ _ (ModuleCat R) |>.obj X)
         (forget₂ _ (ModuleCat R) |>.obj Y)
         (forget₂ _ (ModuleCat R) |>.obj Z)).inv := by
   rfl
 
-end instMonoidalCategory
-
-open instMonoidalCategory
-
 set_option maxHeartbeats 800000 in
 noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R) :=
   Monoidal.induced
     (forget₂ (AlgebraCat R) (ModuleCat R))
-    { tensorObj := instMonoidalCategory.tensorObj
-      μIsoSymm := fun X Y => Iso.refl _
-      whiskerLeft := fun X _ _ f => tensorHom (𝟙 _) f
-      whiskerRight := @fun X₁ X₂ (f : X₁ ⟶ X₂) Y => tensorHom f (𝟙 _)
-      tensorHom := tensorHom
-      tensorUnit' := tensorUnit
+    { μIsoSymm := fun X Y => Iso.refl _
       εIsoSymm := Iso.refl _
-      associator := associator
       associator_eq := fun X Y Z => by
         dsimp only [forget₂_module_obj, forget₂_map_associator_hom]
         simp only [eqToIso_refl, Iso.refl_trans, Iso.refl_symm, Iso.trans_hom, tensorIso_hom,
           Iso.refl_hom, MonoidalCategory.tensor_id]
         erw [Category.id_comp, Category.comp_id, MonoidalCategory.tensor_id, Category.comp_id]
-      leftUnitor := fun X => (Algebra.TensorProduct.lid R X).toAlgebraIso
-      rightUnitor := fun X => (Algebra.TensorProduct.rid R R X).toAlgebraIso
       rightUnitor_eq := fun X => by
         dsimp
         erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]
@@ -99,8 +91,9 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R
 
 variable (R) in
 /-- `forget₂ (AlgebraCat R) (ModuleCat R)` as a monoidal functor. -/
-def toModuleCatMonoidalFunctor : MonoidalFunctor (AlgebraCat.{u} R) (ModuleCat.{u} R) :=
-  Monoidal.fromInduced (forget₂ (AlgebraCat R) (ModuleCat R)) _
+def toModuleCatMonoidalFunctor : MonoidalFunctor (AlgebraCat.{u} R) (ModuleCat.{u} R) := by
+  unfold instMonoidalCategory
+  exact Monoidal.fromInduced (forget₂ (AlgebraCat R) (ModuleCat R)) _
 
 instance : Faithful (toModuleCatMonoidalFunctor R).toFunctor :=
   forget₂_faithful _ _

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

@@ -92,6 +92,26 @@ def associator (M : ModuleCat.{v} R) (N : ModuleCat.{w} R) (K : ModuleCat.{x} R)
   (TensorProduct.assoc R M N K).toModuleIso
 #align Module.monoidal_category.associator ModuleCat.MonoidalCategory.associator
 
+/-- (implementation) the left unitor for R-modules -/
+def leftUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (R ⊗[R] M) ≅ M :=
+  (LinearEquiv.toModuleIso (TensorProduct.lid R M) : of R (R ⊗ M) ≅ of R M).trans (ofSelfIso M)
+#align Module.monoidal_category.left_unitor ModuleCat.MonoidalCategory.leftUnitor
+
+/-- (implementation) the right unitor for R-modules -/
+def rightUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (M ⊗[R] R) ≅ M :=
+  (LinearEquiv.toModuleIso (TensorProduct.rid R M) : of R (M ⊗ R) ≅ of R M).trans (ofSelfIso M)
+#align Module.monoidal_category.right_unitor ModuleCat.MonoidalCategory.rightUnitor
+
+instance : MonoidalCategoryStruct (ModuleCat.{u} R) where
+  tensorObj := tensorObj
+  whiskerLeft := whiskerLeft
+  whiskerRight := whiskerRight
+  tensorHom f g := TensorProduct.map f g
+  tensorUnit := ModuleCat.of R R
+  associator := associator
+  leftUnitor := leftUnitor
+  rightUnitor := rightUnitor
+
 section
 
 /-! The `associator_naturality` and `pentagon` lemmas below are very slow to elaborate.
@@ -143,11 +163,6 @@ theorem pentagon (W X Y Z : ModuleCat R) :
   convert pentagon_aux R W X Y Z using 1
 #align Module.monoidal_category.pentagon ModuleCat.MonoidalCategory.pentagon
 
-/-- (implementation) the left unitor for R-modules -/
-def leftUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (R ⊗[R] M) ≅ M :=
-  (LinearEquiv.toModuleIso (TensorProduct.lid R M) : of R (R ⊗ M) ≅ of R M).trans (ofSelfIso M)
-#align Module.monoidal_category.left_unitor ModuleCat.MonoidalCategory.leftUnitor
-
 theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
     tensorHom (𝟙 (ModuleCat.of R R)) f ≫ (leftUnitor N).hom = (leftUnitor M).hom ≫ f := by
   -- Porting note: broken ext
@@ -162,11 +177,6 @@ theorem leftUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
   rfl
 #align Module.monoidal_category.left_unitor_naturality ModuleCat.MonoidalCategory.leftUnitor_naturality
 
-/-- (implementation) the right unitor for R-modules -/
-def rightUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (M ⊗[R] R) ≅ M :=
-  (LinearEquiv.toModuleIso (TensorProduct.rid R M) : of R (M ⊗ R) ≅ of R M).trans (ofSelfIso M)
-#align Module.monoidal_category.right_unitor ModuleCat.MonoidalCategory.rightUnitor
-
 theorem rightUnitor_naturality {M N : ModuleCat R} (f : M ⟶ N) :
     tensorHom f (𝟙 (ModuleCat.of R R)) ≫ (rightUnitor N).hom = (rightUnitor M).hom ≫ f := by
   -- Porting note: broken ext
@@ -197,17 +207,8 @@ end MonoidalCategory
 
 open MonoidalCategory
 
+set_option maxHeartbeats 400000 in
 instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCategory.ofTensorHom
-  -- data
-  (tensorObj := MonoidalCategory.tensorObj)
-  (tensorHom := @tensorHom _ _)
-  (whiskerLeft := @whiskerLeft _ _)
-  (whiskerRight := @whiskerRight _ _)
-  (tensorUnit' := ModuleCat.of R R)
-  (associator := associator)
-  (leftUnitor := leftUnitor)
-  (rightUnitor := rightUnitor)
-  -- properties
   (tensor_id := fun M N ↦ tensor_id M N)
   (tensor_comp := fun f g h ↦ MonoidalCategory.tensor_comp f g h)
   (associator_naturality := fun f g h ↦ MonoidalCategory.associator_naturality f g h)

Mathlib/CategoryTheory/Bicategory/End.lean

@@ -41,7 +41,7 @@ instance (X : C) : MonoidalCategory (EndMonoidal X) where
   tensorObj f g := f ≫ g
   whiskerLeft {f g h} η := f ◁ η
   whiskerRight {f g} η h := η ▷ h
-  tensorUnit' := 𝟙 _
+  tensorUnit := 𝟙 _
   associator f g h := α_ f g h
   leftUnitor f := λ_ f
   rightUnitor f := ρ_ f