refactor(CategoryTheory/Monoidal): add whiskering operators

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -268,15 +268,15 @@ theorem FGModuleCatEvaluation_apply (f : FGModuleCatDual K V) (x : V) :
 set_option maxHeartbeats 1600000 in
 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
 
 -- Porting note: extremely slow, was fast in mathlib3.
 set_option maxHeartbeats 1600000 in
 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

@@ -179,20 +179,23 @@ theorem associativity (X Y Z : Type u) :
     CategoryTheory.associator_hom_apply]
 #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
@@ -221,7 +224,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

@@ -61,6 +61,16 @@ def tensorHom {M N M' N' : ModuleCat R} (f : M ⟶ N) (g : M' ⟶ N') :
   TensorProduct.map f g
 #align Module.monoidal_category.tensor_hom ModuleCat.MonoidalCategory.tensorHom
 
+/-- (implementation) left whiskering for R-modules -/
+def whiskerLeft (M : ModuleCat R) {N₁ N₂ : ModuleCat R} (f : N₁ ⟶ N₂) :
+    tensorObj M N₁ ⟶ tensorObj M N₂ :=
+  f.lTensor M
+
+/-- (implementation) right whiskering for R-modules -/
+def whiskerRight {M₁ M₂ : ModuleCat R} (f : M₁ ⟶ M₂) (N : ModuleCat R) :
+    tensorObj M₁ N ⟶ tensorObj M₂ N :=
+  f.rTensor N
+
 theorem tensor_id (M N : ModuleCat R) : tensorHom (𝟙 M) (𝟙 N) = 𝟙 (ModuleCat.of R (M ⊗ N)) := by
   -- Porting note: even with high priority ext fails to find this
   apply TensorProduct.ext
@@ -105,9 +115,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
@@ -127,8 +137,8 @@ theorem associator_naturality {X₁ X₂ X₃ Y₁ Y₂ Y₃ : ModuleCat R} (f
 -- Porting note: very slow!
 set_option maxHeartbeats 1600000 in
 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
@@ -187,22 +197,24 @@ end MonoidalCategory
 
 open MonoidalCategory
 
-instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) where
+instance monoidalCategory : MonoidalCategory (ModuleCat.{u} R) := MonoidalCategory.ofTensorHom
   -- data
-  tensorObj := tensorObj
-  tensorHom := @tensorHom _ _
-  tensorUnit' := ModuleCat.of R R
-  associator := associator
-  leftUnitor := leftUnitor
-  rightUnitor := rightUnitor
+  (tensorObj := MonoidalCategory.tensorObj)
+  (tensorHom := @tensorHom _ _)
+  (whiskerLeft := @whiskerLeft _ _)
+  (whiskerRight := @whiskerRight _ _)
+  (tensorUnit' := ModuleCat.of R R)
+  (associator := associator)
+  (leftUnitor := leftUnitor)
+  (rightUnitor := rightUnitor)
   -- properties
-  tensor_id M N := tensor_id M N
-  tensor_comp f g h := MonoidalCategory.tensor_comp f g h
-  associator_naturality f g h := MonoidalCategory.associator_naturality f g h
-  leftUnitor_naturality f := MonoidalCategory.leftUnitor_naturality f
-  rightUnitor_naturality f := rightUnitor_naturality f
-  pentagon M N K L := pentagon M N K L
-  triangle M N := triangle M N
+  (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)
+  (leftUnitor_naturality := fun f ↦ MonoidalCategory.leftUnitor_naturality f)
+  (rightUnitor_naturality := fun f ↦ rightUnitor_naturality f)
+  (pentagon := fun M N K L ↦ pentagon M N K L)
+  (triangle := fun M N ↦ triangle M N)
 #align Module.monoidal_category ModuleCat.monoidalCategory
 
 /-- Remind ourselves that the monoidal unit, being just `R`, is still a commutative ring. -/
@@ -217,6 +229,18 @@ theorem hom_apply {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K
   rfl
 #align Module.monoidal_category.hom_apply ModuleCat.MonoidalCategory.hom_apply
 
+@[simp]
+theorem whiskerLeft_apply (L : ModuleCat.{u} R) {M N : ModuleCat.{u} R} (f : M ⟶ N)
+    (l : L) (m : M) :
+      (L ◁ f) (l ⊗ₜ m) = l ⊗ₜ f m :=
+  rfl
+
+@[simp]
+theorem whiskerRight_apply {L M : ModuleCat.{u} R} (f : L ⟶ M) (N : ModuleCat.{u} R)
+    (l : L) (n : N) :
+      (f ▷ N) (l ⊗ₜ n) = f l ⊗ₜ n :=
+  rfl
+
 @[simp]
 theorem leftUnitor_hom_apply {M : ModuleCat.{u} R} (r : R) (m : M) :
     ((λ_ M).hom : 𝟙_ (ModuleCat R) ⊗ M ⟶ M) (r ⊗ₜ[R] m) = r • m :=
@@ -263,24 +287,24 @@ instance : MonoidalPreadditive (ModuleCat.{u} R) := by
   · 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, MonoidalCategory.hom_apply, LinearMap.zero_apply,
+    rw [LinearMap.zero_apply, ← id_tensorHom, MonoidalCategory.hom_apply, 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, MonoidalCategory.hom_apply, LinearMap.zero_apply,
+    rw [LinearMap.zero_apply, ← tensorHom_id, MonoidalCategory.hom_apply, 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, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
-    erw [MonoidalCategory.hom_apply]
+    rw [LinearMap.add_apply]
+    repeat rw [← id_tensorHom, MonoidalCategory.hom_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, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply]
-    erw [MonoidalCategory.hom_apply]
+    rw [LinearMap.add_apply]
+    repeat rw [← tensorHom_id, MonoidalCategory.hom_apply]
     rw [LinearMap.add_apply, TensorProduct.add_tmul]
 
 -- Porting note: simp wasn't firing but rw was, annoying
@@ -289,12 +313,14 @@ instance : MonoidalLinear R (ModuleCat.{u} R) := by
   · 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, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply,
+    rw [LinearMap.smul_apply, ← id_tensorHom, MonoidalCategory.hom_apply,
+      ← id_tensorHom, MonoidalCategory.hom_apply,
       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, MonoidalCategory.hom_apply, MonoidalCategory.hom_apply,
+    rw [LinearMap.smul_apply, ← tensorHom_id, MonoidalCategory.hom_apply,
+      ← tensorHom_id, MonoidalCategory.hom_apply,
       LinearMap.smul_apply, TensorProduct.smul_tmul, TensorProduct.tmul_smul]
 
 end ModuleCat

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

@@ -38,10 +38,22 @@ theorem braiding_naturality {X₁ X₂ Y₁ Y₂ : ModuleCat.{u} R} (f : X₁ 
 set_option linter.uppercaseLean3 false in
 #align Module.monoidal_category.braiding_naturality ModuleCat.MonoidalCategory.braiding_naturality
 
+@[simp]
+theorem braiding_naturality_left {X Y : ModuleCat R} (f : X ⟶ Y) (Z : ModuleCat R) :
+    f ▷ Z ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ Z ◁ f := by
+  simp_rw [← id_tensorHom, tensorHom_id]
+  apply braiding_naturality
+
+@[simp]
+theorem braiding_naturality_right (X : ModuleCat R) {Y Z : ModuleCat R} (f : Y ⟶ Z) :
+    X ◁ f ≫ (braiding X Z).hom = (braiding X Y).hom ≫ f ▷ X := by
+  simp_rw [← id_tensorHom, tensorHom_id]
+  apply braiding_naturality
+
 @[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
@@ -51,7 +63,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
@@ -64,7 +76,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

@@ -39,15 +39,12 @@ open Bicategory
 attribute [local simp] EndMonoidal in
 instance (X : C) : MonoidalCategory (EndMonoidal X) where
   tensorObj f g := f ≫ g
-  tensorHom {f g} h i η θ := η ▷ h ≫ g ◁ θ
+  whiskerLeft {f g h} η := f ◁ η
+  whiskerRight {f g} η h := η ▷ h
   tensorUnit' := 𝟙 _
   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,8 +41,10 @@ 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]
-      simp }
+      rw [coev_app_comp_pre_app_assoc, ← Functor.map_comp,
+        tensorHom_def, ← comp_whiskerRight_assoc, IsIso.inv_hom_id]
+      simp
+       }
 #align category_theory.functor.closed_unit CategoryTheory.Functor.closedUnit
 
 /-- Auxiliary definition for `CategoryTheory.Functor.closed`.
@@ -55,8 +57,11 @@ 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]
-      simp }
+      rw [tensorHom_def]
+      simp only [NatTrans.naturality, MonoidalCategory.whiskerLeft_comp, Category.assoc,
+        ihom.ev_naturality, comp_obj, tensorLeft_obj, id_obj, id_tensor_pre_app_comp_ev_assoc]
+      simp [← comp_whiskerRight_assoc]
+       }
 #align category_theory.functor.closed_counit CategoryTheory.Functor.closedCounit
 
 /-- If `C` is a monoidal closed category and `D` is a groupoid, then every functor `F : D ⥤ C` is

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