refactor(CategoryTheory/Monoidal): replace axioms with those more sui…

…table for the whiskerings (#9991)

Extracted from #6307. We replace some axioms by those more preferable when using the whiskerings instead of the tensor of morphisms.

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

@@ -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/Monoidal/Braided.lean

@@ -40,11 +40,16 @@ which is natural in both arguments,
 and also satisfies the two hexagon identities.
 -/
 class BraidedCategory (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C] where
-  -- braiding natural iso:
+  /-- braiding natural isomorphism -/
   braiding : ∀ X Y : C, X ⊗ Y ≅ Y ⊗ X
-  braiding_naturality :
-    ∀ {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
-      (f ⊗ g) ≫ (braiding Y Y').hom = (braiding X X').hom ≫ (g ⊗ f) := by
+  -- Note: `𝟙 X ⊗ f` will be replaced by `X ◁ f` (and similarly for `f ⊗ 𝟙 Z`) in #6307.
+  braiding_naturality_right :
+    ∀ (X : C) {Y Z : C} (f : Y ⟶ Z),
+      (𝟙 X ⊗ f) ≫ (braiding X Z).hom = (braiding X Y).hom ≫ (f ⊗ 𝟙 X) := by
+    aesop_cat
+  braiding_naturality_left :
+    ∀ {X Y : C} (f : X ⟶ Y) (Z : C),
+      (f ⊗ 𝟙 Z) ≫ (braiding Y Z).hom = (braiding X Z).hom ≫ (𝟙 Z ⊗ f) := by
     aesop_cat
   -- hexagon identities:
   hexagon_forward :
@@ -59,7 +64,9 @@ class BraidedCategory (C : Type u) [Category.{v} C] [MonoidalCategory.{v} C] whe
     aesop_cat
 #align category_theory.braided_category CategoryTheory.BraidedCategory
 
-attribute [reassoc (attr := simp)] BraidedCategory.braiding_naturality
+attribute [reassoc (attr := simp)]
+  BraidedCategory.braiding_naturality_left
+  BraidedCategory.braiding_naturality_right
 attribute [reassoc] BraidedCategory.hexagon_forward BraidedCategory.hexagon_reverse
 
 open Category
@@ -68,7 +75,54 @@ open MonoidalCategory
 
 open BraidedCategory
 
-notation "β_" => braiding
+notation "β_" => BraidedCategory.braiding
+
+namespace BraidedCategory
+
+variable {C : Type u} [Category.{v} C] [MonoidalCategory.{v} C] [BraidedCategory.{v} C]
+
+@[simp]
+theorem braiding_tensor_left (X Y Z : C) :
+    (β_ (X ⊗ Y) Z).hom  =
+      (α_ X Y Z).hom ≫ (𝟙 X ⊗ (β_ Y Z).hom) ≫ (α_ X Z Y).inv ≫
+        ((β_ X Z).hom ⊗ 𝟙 Y) ≫ (α_ Z X Y).hom := by
+  intros
+  apply (cancel_epi (α_ X Y Z).inv).1
+  apply (cancel_mono (α_ Z X Y).inv).1
+  simp [hexagon_reverse]
+
+@[simp]
+theorem braiding_tensor_right (X Y Z : C) :
+    (β_ X (Y ⊗ Z)).hom  =
+      (α_ X Y Z).inv ≫ ((β_ X Y).hom ⊗ 𝟙 Z) ≫ (α_ Y X Z).hom ≫
+        (𝟙 Y ⊗ (β_ X Z).hom) ≫ (α_ Y Z X).inv := by
+  intros
+  apply (cancel_epi (α_ X Y Z).hom).1
+  apply (cancel_mono (α_ Y Z X).hom).1
+  simp [hexagon_forward]
+
+@[simp]
+theorem braiding_inv_tensor_left (X Y Z : C) :
+    (β_ (X ⊗ Y) Z).inv  =
+      (α_ Z X Y).inv ≫ ((β_ X Z).inv ⊗ 𝟙 Y) ≫ (α_ X Z Y).hom ≫
+        (𝟙 X ⊗ (β_ Y Z).inv) ≫ (α_ X Y Z).inv :=
+  eq_of_inv_eq_inv (by simp)
+
+@[simp]
+theorem braiding_inv_tensor_right (X Y Z : C) :
+    (β_ X (Y ⊗ Z)).inv  =
+      (α_ Y Z X).hom ≫ (𝟙 Y ⊗ (β_ X Z).inv) ≫ (α_ Y X Z).inv ≫
+        ((β_ X Y).inv ⊗ 𝟙 Z) ≫ (α_ X Y Z).hom :=
+  eq_of_inv_eq_inv (by simp)
+
+-- The priority setting will not be needed when we replace `𝟙 X ⊗ f` by `X ◁ f`.
+@[reassoc (attr := simp (low))]
+theorem braiding_naturality {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
+    (f ⊗ g) ≫ (braiding Y Y').hom = (braiding X X').hom ≫ (g ⊗ f) := by
+  rw [← tensor_id_comp_id_tensor f g, ← id_tensor_comp_tensor_id g f]
+  simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]
+
+end BraidedCategory
 
 /--
 Verifying the axioms for a braiding by checking that the candidate braiding is sent to a braiding
@@ -79,12 +133,18 @@ def braidedCategoryOfFaithful {C D : Type*} [Category C] [Category D] [MonoidalC
     (β : ∀ X Y : C, X ⊗ Y ≅ Y ⊗ X)
     (w : ∀ X Y, F.μ _ _ ≫ F.map (β X Y).hom = (β_ _ _).hom ≫ F.μ _ _) : BraidedCategory C where
   braiding := β
-  braiding_naturality := by
+  braiding_naturality_left := by
+    intros
+    apply F.map_injective
+    refine (cancel_epi (F.μ ?_ ?_)).1 ?_
+    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_left_assoc, w, Functor.map_comp,
+      reassoc_of% w, braiding_naturality_left_assoc, LaxMonoidalFunctor.μ_natural_right]
+  braiding_naturality_right := by
     intros
     apply F.map_injective
     refine (cancel_epi (F.μ ?_ ?_)).1 ?_
-    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_assoc, w, Functor.map_comp, reassoc_of% w,
-      braiding_naturality_assoc, LaxMonoidalFunctor.μ_natural]
+    rw [Functor.map_comp, ← LaxMonoidalFunctor.μ_natural_right_assoc, w, Functor.map_comp,
+      reassoc_of% w, braiding_naturality_right_assoc, LaxMonoidalFunctor.μ_natural_left]
   hexagon_forward := by
     intros
     apply F.map_injective

Mathlib/CategoryTheory/Monoidal/Center.lean

@@ -325,11 +325,6 @@ def braiding (X Y : Center C) : X ⊗ Y ≅ Y ⊗ X :=
 
 instance braidedCategoryCenter : BraidedCategory (Center C) where
   braiding := braiding
-  braiding_naturality f g := by
-    ext
-    dsimp
-    rw [← tensor_id_comp_id_tensor, Category.assoc, HalfBraiding.naturality, f.comm_assoc,
-      id_tensor_comp_tensor_id]
 #align category_theory.center.braided_category_center CategoryTheory.Center.braidedCategoryCenter
 
 -- `aesop_cat` handles the hexagon axioms

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -260,6 +260,14 @@ theorem map_tensor {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') :
     F.map (f ⊗ g) = inv (F.μ X X') ≫ (F.map f ⊗ F.map g) ≫ F.μ Y Y' := by simp
 #align category_theory.monoidal_functor.map_tensor CategoryTheory.MonoidalFunctor.map_tensor
 
+-- Note: `𝟙 X ⊗ f` will be replaced by `X ◁ f` in #6307.
+theorem map_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) :
+    F.map (𝟙 X ⊗ f) = inv (F.μ X Y) ≫ (𝟙 (F.obj X) ⊗ F.map f) ≫ F.μ X Z := by simp
+
+-- Note: `f ⊗ 𝟙 Z` will be replaced by `f ▷ Z` in #6307.
+theorem map_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) :
+    F.map (f ⊗ 𝟙 Z) = inv (F.μ X Z) ≫ (F.map f ⊗ 𝟙 (F.obj Z)) ≫ F.μ Y Z := by simp
+
 theorem map_leftUnitor (X : C) :
     F.map (λ_ X).hom = inv (F.μ (𝟙_ C) X) ≫ (inv F.ε ⊗ 𝟙 (F.obj X)) ≫ (λ_ (F.obj X)).hom := by
   simp only [LaxMonoidalFunctor.left_unitality]

Mathlib/CategoryTheory/Monoidal/OfChosenFiniteProducts/Symmetric.lean

@@ -93,7 +93,8 @@ open MonoidalOfChosenFiniteProducts
 def symmetricOfChosenFiniteProducts : SymmetricCategory (MonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ)
     where
   braiding _ _ := Limits.BinaryFan.braiding (ℬ _ _).isLimit (ℬ _ _).isLimit
-  braiding_naturality f g := braiding_naturality ℬ f g
+  braiding_naturality_left f X := braiding_naturality ℬ f (𝟙 X)
+  braiding_naturality_right X _ _ f := braiding_naturality ℬ (𝟙 X) f
   hexagon_forward X Y Z := hexagon_forward ℬ X Y Z
   hexagon_reverse X Y Z := hexagon_reverse ℬ X Y Z
   symmetry X Y := symmetry ℬ X Y

Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

@@ -130,7 +130,8 @@ open MonoidalCategory
 @[simps]
 def symmetricOfHasFiniteProducts [HasTerminal C] [HasBinaryProducts C] : SymmetricCategory C where
   braiding X Y := Limits.prod.braiding X Y
-  braiding_naturality f g := by dsimp [tensorHom]; simp
+  braiding_naturality_left f X := by simp
+  braiding_naturality_right X _ _ f := by simp
   hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteProducts.associator_hom]; simp
   hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteProducts.associator_inv]; simp
   symmetry X Y := by dsimp; simp
@@ -226,7 +227,8 @@ open MonoidalCategory
 def symmetricOfHasFiniteCoproducts [HasInitial C] [HasBinaryCoproducts C] :
     SymmetricCategory C where
   braiding := Limits.coprod.braiding
-  braiding_naturality f g := by dsimp [tensorHom]; simp
+  braiding_naturality_left f g := by simp
+  braiding_naturality_right f g := by simp
   hexagon_forward X Y Z := by dsimp [monoidalOfHasFiniteCoproducts.associator_hom]; simp
   hexagon_reverse X Y Z := by dsimp [monoidalOfHasFiniteCoproducts.associator_inv]; simp
   symmetry X Y := by dsimp; simp

Mathlib/CategoryTheory/Monoidal/Preadditive.lean

@@ -34,24 +34,42 @@ Note we don't `extend Preadditive C` here, as `Abelian C` already extends it,
 and we'll need to have both typeclasses sometimes.
 -/
 class MonoidalPreadditive : Prop where
-  /-- tensoring on the right with a zero morphism gives zero -/
-  tensor_zero : ∀ {W X Y Z : C} (f : W ⟶ X), f ⊗ (0 : Y ⟶ Z) = 0 := by aesop_cat
-  /-- tensoring on the left with a zero morphism gives zero -/
-  zero_tensor : ∀ {W X Y Z : C} (f : Y ⟶ Z), (0 : W ⟶ X) ⊗ f = 0 := by aesop_cat
-  /-- left tensoring with a morphism is compatible with addition -/
-  tensor_add : ∀ {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z), f ⊗ (g + h) = f ⊗ g + f ⊗ h := by
-    aesop_cat
-  /-- right tensoring with a morphism is compatible with addition -/
-  add_tensor : ∀ {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z), (f + g) ⊗ h = f ⊗ h + g ⊗ h := by
-    aesop_cat
+  -- Note: `𝟙 X ⊗ f` will be replaced by `X ◁ f` (and similarly for `f ⊗ 𝟙 X`) in #6307.
+  whiskerLeft_zero : ∀ {X Y Z : C}, 𝟙 X ⊗ (0 : Y ⟶ Z) = 0 := by aesop_cat
+  zero_whiskerRight : ∀ {X Y Z : C}, (0 : Y ⟶ Z) ⊗ 𝟙 X = 0 := by aesop_cat
+  whiskerLeft_add : ∀ {X Y Z : C} (f g : Y ⟶ Z), 𝟙 X ⊗ (f + g) = 𝟙 X ⊗ f + 𝟙 X ⊗ g := by aesop_cat
+  add_whiskerRight : ∀ {X Y Z : C} (f g : Y ⟶ Z), (f + g) ⊗ 𝟙 X = f ⊗ 𝟙 X + g ⊗ 𝟙 X := by aesop_cat
 #align category_theory.monoidal_preadditive CategoryTheory.MonoidalPreadditive
 
-attribute [simp] MonoidalPreadditive.tensor_zero MonoidalPreadditive.zero_tensor
+attribute [simp] MonoidalPreadditive.whiskerLeft_zero MonoidalPreadditive.zero_whiskerRight
+attribute [simp] MonoidalPreadditive.whiskerLeft_add MonoidalPreadditive.add_whiskerRight
 
 variable {C}
 variable [MonoidalPreadditive C]
 
-attribute [local simp] MonoidalPreadditive.tensor_add MonoidalPreadditive.add_tensor
+namespace MonoidalPreadditive
+
+-- The priority setting will not be needed when we replace `𝟙 X ⊗ f` by `X ◁ f`.
+@[simp (low)]
+theorem tensor_zero {W X Y Z : C} (f : W ⟶ X) : f ⊗ (0 : Y ⟶ Z) = 0 := by
+  rw [← tensor_id_comp_id_tensor]
+  simp
+
+-- The priority setting will not be needed when we replace `f ⊗ 𝟙 X` by `f ▷ X`.
+@[simp (low)]
+theorem zero_tensor {W X Y Z : C} (f : Y ⟶ Z) : (0 : W ⟶ X) ⊗ f = 0 := by
+  rw [← tensor_id_comp_id_tensor]
+  simp
+
+theorem tensor_add {W X Y Z : C} (f : W ⟶ X) (g h : Y ⟶ Z) : f ⊗ (g + h) = f ⊗ g + f ⊗ h := by
+  rw [← tensor_id_comp_id_tensor]
+  simp
+
+theorem add_tensor {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z) : (f + g) ⊗ h = f ⊗ h + g ⊗ h := by
+  rw [← tensor_id_comp_id_tensor]
+  simp
+
+end MonoidalPreadditive
 
 instance tensorLeft_additive (X : C) : (tensorLeft X).Additive where
 #align category_theory.tensor_left_additive CategoryTheory.tensorLeft_additive
@@ -70,24 +88,24 @@ ensures that the domain is monoidal preadditive. -/
 theorem monoidalPreadditive_of_faithful {D} [Category D] [Preadditive D] [MonoidalCategory D]
     (F : MonoidalFunctor D C) [Faithful F.toFunctor] [F.toFunctor.Additive] :
     MonoidalPreadditive D :=
-  { tensor_zero := by
+  { whiskerLeft_zero := by
       intros
       apply F.toFunctor.map_injective
-      simp [F.map_tensor]
-    zero_tensor := by
+      simp [F.map_whiskerLeft]
+    zero_whiskerRight := by
       intros
       apply F.toFunctor.map_injective
-      simp [F.map_tensor]
-    tensor_add := by
+      simp [F.map_whiskerRight]
+    whiskerLeft_add := by
       intros
       apply F.toFunctor.map_injective
-      simp only [F.map_tensor, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
-        MonoidalPreadditive.tensor_add]
-    add_tensor := by
+      simp only [F.map_whiskerLeft, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
+        MonoidalPreadditive.whiskerLeft_add]
+    add_whiskerRight := by
       intros
       apply F.toFunctor.map_injective
-      simp only [F.map_tensor, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
-        MonoidalPreadditive.add_tensor] }
+      simp only [F.map_whiskerRight, Functor.map_add, Preadditive.comp_add, Preadditive.add_comp,
+        MonoidalPreadditive.add_whiskerRight] }
 #align category_theory.monoidal_preadditive_of_faithful CategoryTheory.monoidalPreadditive_of_faithful
 
 open BigOperators