refactor(CategoryTheory/Monoidal): add whiskering operators

Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean

@@ -83,6 +83,11 @@ noncomputable instance instMonoidalCategory : MonoidalCategory (AlgebraCat.{u} R
         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.id_comp]
+      leftUnitor_eq := fun X => by
+        dsimp only [forget₂_module_obj, forget₂_module_map, Iso.refl_symm, Iso.trans_hom,
+          Iso.refl_hom, tensorIso_hom]
+        simp only [MonoidalCategory.leftUnitor_conjugation, Category.id_comp, Iso.hom_inv_id]
+        rfl
       rightUnitor_eq := fun X => by
         dsimp
         erw [Category.id_comp, MonoidalCategory.tensor_id, Category.id_comp]

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -266,13 +266,13 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
 
 private theorem coevaluation_evaluation :
     letI V' : FGModuleCat K := FGModuleCatDual K V
-    (𝟙 V' ⊗ FGModuleCatCoevaluation K V) ≫ (α_ V' V V').inv ≫ (FGModuleCatEvaluation K V ⊗ 𝟙 V') =
+    (V' ◁ FGModuleCatCoevaluation K V) ≫ (α_ V' V V').inv ≫ (FGModuleCatEvaluation K V ▷ V') =
       (ρ_ V').hom ≫ (λ_ V').inv := by
   apply contractLeft_assoc_coevaluation K V
 
 private theorem evaluation_coevaluation :
-    (FGModuleCatCoevaluation K V ⊗ 𝟙 V) ≫
-        (α_ V (FGModuleCatDual K V) V).hom ≫ (𝟙 V ⊗ FGModuleCatEvaluation K V) =
+    (FGModuleCatCoevaluation K V ▷ V) ≫
+        (α_ V (FGModuleCatDual K V) V).hom ≫ (V ◁ FGModuleCatEvaluation K V) =
       (λ_ V).hom ≫ (ρ_ V).inv := by
   apply contractLeft_assoc_coevaluation' K V
 

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -183,20 +183,23 @@ theorem associativity (X Y Z : Type u) :
     CategoryTheory.associator_hom_apply]; rfl
 #align Module.free.associativity ModuleCat.Free.associativity
 
--- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
-/-- The free R-module functor is lax monoidal. -/
+/-- The free R-module functor is lax monoidal. The structure part. -/
 @[simps]
-instance : LaxMonoidal.{u} (free R).obj where
+instance : LaxMonoidalStruct.{u} (free R).obj where
   -- Send `R` to `PUnit →₀ R`
   ε := ε R
   -- Send `(α →₀ R) ⊗ (β →₀ R)` to `α × β →₀ R`
   μ X Y := (μ R X Y).hom
-  μ_natural {_} {_} {_} {_} f g := μ_natural R f g
-  left_unitality := left_unitality R
-  right_unitality := right_unitality R
-  associativity := associativity R
 
-instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
+-- In fact, it's strong monoidal, but we don't yet have a typeclass for that.
+/-- The free R-module functor is lax monoidal. The property part. -/
+instance : LaxMonoidal.{u} (free R).obj := .ofTensorHom
+  (μ_natural := fun {_} {_} {_} {_} f g ↦ μ_natural R f g)
+  (left_unitality := left_unitality R)
+  (right_unitality := right_unitality R)
+  (associativity := associativity R)
+
+instance : IsIso (@LaxMonoidalStruct.ε _ _ _ _ _ _ (free R).obj _ _) := by
   refine' ⟨⟨Finsupp.lapply PUnit.unit, ⟨_, _⟩⟩⟩
   · -- Porting note: broken ext
     apply LinearMap.ext_ring
@@ -225,7 +228,7 @@ variable [CommRing R]
 def monoidalFree : MonoidalFunctor (Type u) (ModuleCat.{u} R) :=
   { LaxMonoidalFunctor.of (free R).obj with
     -- Porting note: used to be dsimp
-    ε_isIso := (by infer_instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _))
+    ε_isIso := inferInstanceAs <| IsIso LaxMonoidalStruct.ε
     μ_isIso := fun X Y => by dsimp; infer_instance }
 #align Module.monoidal_free ModuleCat.monoidalFree
 

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

@@ -137,9 +137,9 @@ variable (R)
 
 private theorem pentagon_aux (W X Y Z : Type*) [AddCommMonoid W] [AddCommMonoid X]
     [AddCommMonoid Y] [AddCommMonoid Z] [Module R W] [Module R X] [Module R Y] [Module R Z] :
-    ((map (1 : W →ₗ[R] W) (assoc R X Y Z).toLinearMap).comp
+    (((assoc R X Y Z).toLinearMap.lTensor W).comp
             (assoc R W (X ⊗[R] Y) Z).toLinearMap).comp
-        (map ↑(assoc R W X Y) (1 : Z →ₗ[R] Z)) =
+        ((assoc R W X Y).rTensor Z) =
       (assoc R W X (Y ⊗[R] Z)).toLinearMap.comp (assoc R (W ⊗[R] X) Y Z).toLinearMap := by
   apply TensorProduct.ext_fourfold
   intro w x y z
@@ -157,8 +157,8 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f
 #align Module.monoidal_category.associator_naturality ModuleCat.MonoidalCategory.associator_naturality
 
 theorem pentagon (W X Y Z : ModuleCat R) :
-    tensorHom (associator W X Y).hom (𝟙 Z) ≫
-        (associator W (tensorObj X Y) Z).hom ≫ tensorHom (𝟙 W) (associator X Y Z).hom =
+    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
   convert pentagon_aux R W X Y Z using 1
 #align Module.monoidal_category.pentagon ModuleCat.MonoidalCategory.pentagon
@@ -290,30 +290,30 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.zero_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerLeft_apply]
     rw [LinearMap.zero_apply, TensorProduct.tmul_zero]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.zero_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerRight_apply]
     rw [LinearMap.zero_apply, TensorProduct.zero_tmul]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.add_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
+    erw [MonoidalCategory.whiskerLeft_apply]
     rw [LinearMap.add_apply, TensorProduct.tmul_add]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.add_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
-    erw [MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
+    erw [MonoidalCategory.whiskerRight_apply]
     rw [LinearMap.add_apply, TensorProduct.add_tmul]
 
 -- Porting note: simp wasn't firing but rw was, annoying
@@ -324,14 +324,14 @@ instance : MonoidalLinear R (ModuleCat.{u} R) := by
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.smul_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
     rw [LinearMap.smul_apply, TensorProduct.tmul_smul]
   · dsimp only [autoParam]; intros
     refine' TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => _)
     simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply]
     rw [LinearMap.smul_apply]
     -- This used to be `rw`, but we need `erw` after leanprover/lean4#2644
-    erw [MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
+    erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
     rw [LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul]
 
 end ModuleCat

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

@@ -54,7 +54,7 @@ theorem braiding_naturality_right (X : ModuleCat R) {Y Z : ModuleCat R} (f : Y 
 @[simp]
 theorem hexagon_forward (X Y Z : ModuleCat.{u} R) :
     (α_ X Y Z).hom ≫ (braiding X _).hom ≫ (α_ Y Z X).hom =
-      ((braiding X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫ (𝟙 Y ⊗ (braiding X Z).hom) := by
+      ((braiding X Y).hom ▷ Z) ≫ (α_ Y X Z).hom ≫ (Y ◁ (braiding X Z).hom) := by
   apply TensorProduct.ext_threefold
   intro x y z
   rfl
@@ -64,7 +64,7 @@ set_option linter.uppercaseLean3 false in
 @[simp]
 theorem hexagon_reverse (X Y Z : ModuleCat.{u} R) :
     (α_ X Y Z).inv ≫ (braiding _ Z).hom ≫ (α_ Z X Y).inv =
-      (𝟙 X ⊗ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ⊗ 𝟙 Y) := by
+      (X ◁ (Y.braiding Z).hom) ≫ (α_ X Z Y).inv ≫ ((X.braiding Z).hom ▷ Y) := by
   apply (cancel_epi (α_ X Y Z).hom).1
   apply TensorProduct.ext_threefold
   intro x y z
@@ -77,7 +77,8 @@ attribute [local ext] TensorProduct.ext
 /-- The symmetric monoidal structure on `Module R`. -/
 instance symmetricCategory : SymmetricCategory (ModuleCat.{u} R) where
   braiding := braiding
-  braiding_naturality f g := braiding_naturality f g
+  braiding_naturality_left := braiding_naturality_left
+  braiding_naturality_right := braiding_naturality_right
   hexagon_forward := hexagon_forward
   hexagon_reverse := hexagon_reverse
   -- porting note: this proof was automatic in Lean3

Mathlib/CategoryTheory/Bicategory/End.lean

@@ -45,10 +45,6 @@ instance (X : C) : MonoidalCategory (EndMonoidal X) where
   associator f g h := α_ f g h
   leftUnitor f := λ_ f
   rightUnitor f := ρ_ f
-  tensor_comp := by
-    intros
-    dsimp
-    rw [Bicategory.whiskerLeft_comp, Bicategory.comp_whiskerRight, Category.assoc, Category.assoc,
-      Bicategory.whisker_exchange_assoc]
+  whisker_exchange := whisker_exchange
 
 end CategoryTheory

Mathlib/CategoryTheory/Bicategory/SingleObj.lean

@@ -53,18 +53,12 @@ instance : Bicategory (MonoidalSingleObj C) where
   Hom _ _ := C
   id _ := 𝟙_ C
   comp X Y := tensorObj X Y
-  whiskerLeft X Y Z f := tensorHom (𝟙 X) f
-  whiskerRight f Z := tensorHom f (𝟙 Z)
+  whiskerLeft X Y Z f := X ◁ f
+  whiskerRight f Z := f ▷ Z
   associator X Y Z := α_ X Y Z
   leftUnitor X := λ_ X
   rightUnitor X := ρ_ X
-  comp_whiskerLeft _ _ _ _ _ := by
-    simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc, tensor_id]
-  whisker_assoc _ _ _ _ _ := by simp_rw [associator_inv_naturality, Iso.hom_inv_id_assoc]
-  whiskerRight_comp _ _ _ := by simp_rw [← tensor_id, associator_naturality, Iso.inv_hom_id_assoc]
-  id_whiskerLeft _ := by simp_rw [leftUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-  whiskerRight_id _ := by simp_rw [rightUnitor_inv_naturality, Iso.hom_inv_id_assoc]
-  pentagon _ _ _ _ := by simp_rw [pentagon]
+  whisker_exchange := whisker_exchange
 
 namespace MonoidalSingleObj
 
@@ -86,10 +80,6 @@ def endMonoidalStarFunctor : MonoidalFunctor (EndMonoidal (MonoidalSingleObj.sta
   map f := f
   ε := 𝟙 _
   μ X Y := 𝟙 _
-  μ_natural f g := by
-    simp_rw [Category.id_comp, Category.comp_id]
-    -- Should we provide further simp lemmas so this goal becomes visible?
-    exact (tensor_id_comp_id_tensor _ _).symm
 #align category_theory.monoidal_single_obj.End_monoidal_star_functor CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctor
 
 /-- The equivalence between the endomorphisms of the single object

Mathlib/CategoryTheory/Closed/FunctorCategory.lean

@@ -41,7 +41,7 @@ def closedUnit (F : D ⥤ C) : 𝟭 (D ⥤ C) ⟶ tensorLeft F ⋙ closedIhom F
       dsimp
       simp only [ihom.coev_naturality, closedIhom_obj_map, Monoidal.tensorObj_map]
       dsimp
-      rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp]
+      rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp, tensorHom_def]
       simp }
 #align category_theory.functor.closed_unit CategoryTheory.Functor.closedUnit
 
@@ -55,7 +55,7 @@ def closedCounit (F : D ⥤ C) : closedIhom F ⋙ tensorLeft F ⟶ 𝟭 (D ⥤ C
       intro X Y f
       dsimp
       simp only [closedIhom_obj_map, pre_comm_ihom_map]
-      rw [← tensor_id_comp_id_tensor, id_tensor_comp]
+      rw [tensorHom_def]
       simp }
 #align category_theory.functor.closed_counit CategoryTheory.Functor.closedCounit
 

Mathlib/CategoryTheory/Closed/Ideal.lean

@@ -161,7 +161,7 @@ def cartesianClosedOfReflective : CartesianClosed D :=
                     Adjunction.rightAdjointPreservesLimits.{0, 0} (Adjunction.ofRightAdjoint i)
                   apply asIso (prodComparison i B X)
                 · dsimp [asIso]
-                  rw [prodComparison_natural, Functor.map_id]
+                  erw [prodComparison_natural, Functor.map_id]
               · apply (exponentialIdealReflective i _).symm } } }
 #align category_theory.cartesian_closed_of_reflective CategoryTheory.cartesianClosedOfReflective
 

Mathlib/CategoryTheory/Closed/Monoidal.lean

@@ -119,13 +119,13 @@ theorem ihom_adjunction_unit : (ihom.adjunction A).unit = coev A :=
 
 @[reassoc (attr := simp)]
 theorem ev_naturality {X Y : C} (f : X ⟶ Y) :
-    (𝟙 A ⊗ (ihom A).map f) ≫ (ev A).app Y = (ev A).app X ≫ f :=
+    A ◁ (ihom A).map f ≫ (ev A).app Y = (ev A).app X ≫ f :=
   (ev A).naturality f
 #align category_theory.ihom.ev_naturality CategoryTheory.ihom.ev_naturality
 
 @[reassoc (attr := simp)]
 theorem coev_naturality {X Y : C} (f : X ⟶ Y) :
-    f ≫ (coev A).app Y = (coev A).app X ≫ (ihom A).map (𝟙 A ⊗ f) :=
+    f ≫ (coev A).app Y = (coev A).app X ≫ (ihom A).map (A ◁ f) :=
   (coev A).naturality f
 #align category_theory.ihom.coev_naturality CategoryTheory.ihom.coev_naturality
 
@@ -134,8 +134,8 @@ set_option quotPrecheck false in
 notation A " ⟶[" C "] " B:10 => (@ihom C _ _ A _).obj B
 
 @[reassoc (attr := simp)]
-theorem ev_coev : (𝟙 A ⊗ (coev A).app B) ≫ (ev A).app (A ⊗ B) = 𝟙 (A ⊗ B) :=
-  Adjunction.left_triangle_components (ihom.adjunction A)
+theorem ev_coev : (A ◁ (coev A).app B) ≫ (ev A).app (A ⊗ B) = 𝟙 (A ⊗ B) :=
+  (ihom.adjunction A).left_triangle_components
 #align category_theory.ihom.ev_coev CategoryTheory.ihom.ev_coev
 
 @[reassoc (attr := simp)]
@@ -179,7 +179,7 @@ theorem homEquiv_symm_apply_eq (f : Y ⟶ A ⟶[C] X) :
 #align category_theory.monoidal_closed.hom_equiv_symm_apply_eq CategoryTheory.MonoidalClosed.homEquiv_symm_apply_eq
 
 @[reassoc]
-theorem curry_natural_left (f : X ⟶ X') (g : A ⊗ X' ⟶ Y) : curry ((𝟙 _ ⊗ f) ≫ g) = f ≫ curry g :=
+theorem curry_natural_left (f : X ⟶ X') (g : A ⊗ X' ⟶ Y) : curry (_ ◁ f ≫ g) = f ≫ curry g :=
   Adjunction.homEquiv_naturality_left _ _ _
 #align category_theory.monoidal_closed.curry_natural_left CategoryTheory.MonoidalClosed.curry_natural_left
 
@@ -197,7 +197,7 @@ theorem uncurry_natural_right (f : X ⟶ A ⟶[C] Y) (g : Y ⟶ Y') :
 
 @[reassoc]
 theorem uncurry_natural_left (f : X ⟶ X') (g : X' ⟶ A ⟶[C] Y) :
-    uncurry (f ≫ g) = (𝟙 _ ⊗ f) ≫ uncurry g :=
+    uncurry (f ≫ g) = _ ◁ f ≫ uncurry g :=
   Adjunction.homEquiv_naturality_left_symm _ _ _
 #align category_theory.monoidal_closed.uncurry_natural_left CategoryTheory.MonoidalClosed.uncurry_natural_left
 
@@ -220,7 +220,7 @@ theorem eq_curry_iff (f : A ⊗ Y ⟶ X) (g : Y ⟶ A ⟶[C] X) : g = curry f 
 #align category_theory.monoidal_closed.eq_curry_iff CategoryTheory.MonoidalClosed.eq_curry_iff
 
 -- I don't think these two should be simp.
-theorem uncurry_eq (g : Y ⟶ A ⟶[C] X) : uncurry g = (𝟙 A ⊗ g) ≫ (ihom.ev A).app X :=
+theorem uncurry_eq (g : Y ⟶ A ⟶[C] X) : uncurry g = (A ◁ g) ≫ (ihom.ev A).app X :=
   Adjunction.homEquiv_counit _
 #align category_theory.monoidal_closed.uncurry_eq CategoryTheory.MonoidalClosed.uncurry_eq
 
@@ -239,7 +239,7 @@ theorem uncurry_injective : Function.Injective (uncurry : (Y ⟶ A ⟶[C] X) →
 variable (A X)
 
 theorem uncurry_id_eq_ev : uncurry (𝟙 (A ⟶[C] X)) = (ihom.ev A).app X := by
-  rw [uncurry_eq, tensor_id, id_comp]
+  simp [uncurry_eq]
 #align category_theory.monoidal_closed.uncurry_id_eq_ev CategoryTheory.MonoidalClosed.uncurry_id_eq_ev
 
 theorem curry_id_eq_coev : curry (𝟙 _) = (ihom.coev A).app X := by
@@ -258,19 +258,19 @@ def pre (f : B ⟶ A) : ihom A ⟶ ihom B :=
 
 @[reassoc (attr := simp)]
 theorem id_tensor_pre_app_comp_ev (f : B ⟶ A) (X : C) :
-    (𝟙 B ⊗ (pre f).app X) ≫ (ihom.ev B).app X = (f ⊗ 𝟙 (A ⟶[C] X)) ≫ (ihom.ev A).app X :=
+    B ◁ (pre f).app X ≫ (ihom.ev B).app X = f ▷ (A ⟶[C] X) ≫ (ihom.ev A).app X :=
   transferNatTransSelf_counit _ _ ((tensoringLeft C).map f) X
 #align category_theory.monoidal_closed.id_tensor_pre_app_comp_ev CategoryTheory.MonoidalClosed.id_tensor_pre_app_comp_ev
 
 @[simp]
 theorem uncurry_pre (f : B ⟶ A) (X : C) :
-    MonoidalClosed.uncurry ((pre f).app X) = (f ⊗ 𝟙 _) ≫ (ihom.ev A).app X := by
-  rw [uncurry_eq, id_tensor_pre_app_comp_ev]
+    MonoidalClosed.uncurry ((pre f).app X) = f ▷ _ ≫ (ihom.ev A).app X := by
+  simp [uncurry_eq]
 #align category_theory.monoidal_closed.uncurry_pre CategoryTheory.MonoidalClosed.uncurry_pre
 
 @[reassoc (attr := simp)]
 theorem coev_app_comp_pre_app (f : B ⟶ A) :
-    (ihom.coev A).app X ≫ (pre f).app (A ⊗ X) = (ihom.coev B).app X ≫ (ihom B).map (f ⊗ 𝟙 _) :=
+    (ihom.coev A).app X ≫ (pre f).app (A ⊗ X) = (ihom.coev B).app X ≫ (ihom B).map (f ▷ _) :=
   unit_transferNatTransSelf _ _ ((tensoringLeft C).map f) X
 #align category_theory.monoidal_closed.coev_app_comp_pre_app CategoryTheory.MonoidalClosed.coev_app_comp_pre_app