feat(CategoryTheory/Monoidal): add lemmas for the whiskerings (#9995)

yuma-mizuno · yuma-mizuno · commit f1919fd4e80a · 2024-01-27T14:51:46.000Z
Extracted from #6307.
diff --git a/Mathlib/CategoryTheory/Bicategory/Basic.lean b/Mathlib/CategoryTheory/Bicategory/Basic.lean
@@ -193,19 +193,19 @@ attribute [simp]
 variable {B : Type u} [Bicategory.{w, v} B] {a b c d e : B}
 
 @[reassoc (attr := simp)]
-theorem hom_inv_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
+theorem whiskerLeft_hom_inv (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
     f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g) := by rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]
-#align category_theory.bicategory.hom_inv_whisker_left CategoryTheory.Bicategory.hom_inv_whiskerLeft
+#align category_theory.bicategory.hom_inv_whisker_left CategoryTheory.Bicategory.whiskerLeft_hom_inv
 
 @[reassoc (attr := simp)]
 theorem hom_inv_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
     η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h) := by rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]
 #align category_theory.bicategory.hom_inv_whisker_right CategoryTheory.Bicategory.hom_inv_whiskerRight
 
 @[reassoc (attr := simp)]
-theorem inv_hom_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
+theorem whiskerLeft_inv_hom (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
     f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h) := by rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]
-#align category_theory.bicategory.inv_hom_whisker_left CategoryTheory.Bicategory.inv_hom_whiskerLeft
+#align category_theory.bicategory.inv_hom_whisker_left CategoryTheory.Bicategory.whiskerLeft_inv_hom
 
 @[reassoc (attr := simp)]
 theorem inv_hom_whiskerRight {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
diff --git a/Mathlib/CategoryTheory/Bicategory/Functor.lean b/Mathlib/CategoryTheory/Bicategory/Functor.lean
@@ -530,7 +530,7 @@ def mkOfOplax (F : OplaxFunctor B C) (F' : F.PseudoCore) : Pseudofunctor B C :=
     map₂_associator := fun f g h => by
       dsimp
       rw [F'.mapCompIso_hom (f ≫ g) h, F'.mapCompIso_hom f g, ← F.map₂_associator_assoc, ←
-        F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, hom_inv_whiskerLeft_assoc,
+        F'.mapCompIso_hom f (g ≫ h), ← F'.mapCompIso_hom g h, whiskerLeft_hom_inv_assoc,
         hom_inv_id, comp_id] }
 #align category_theory.pseudofunctor.mk_of_oplax CategoryTheory.Pseudofunctor.mkOfOplax
 
diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -222,7 +222,79 @@ end MonoidalCategory
 open scoped MonoidalCategory
 open MonoidalCategory
 
-variable (C : Type u) [𝒞 : Category.{v} C] [MonoidalCategory C]
+variable {C : Type u} [𝒞 : Category.{v} C] [MonoidalCategory C]
+
+namespace MonoidalCategory
+
+@[reassoc (attr := simp)]
+theorem whiskerLeft_hom_inv (X : C) {Y Z : C} (f : Y ≅ Z) :
+    X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (X ⊗ Y) := by
+  simp [← id_tensorHom, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem hom_inv_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) :
+    f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (X ⊗ Z) := by
+  simp [← tensorHom_id, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem whiskerLeft_inv_hom (X : C) {Y Z : C} (f : Y ≅ Z) :
+    X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (X ⊗ Z) := by
+  simp [← id_tensorHom, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem inv_hom_whiskerRight {X Y : C} (f : X ≅ Y) (Z : C) :
+    f.inv ▷ Z ≫ f.hom ▷ Z = 𝟙 (Y ⊗ Z) := by
+  simp [← tensorHom_id, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem whiskerLeft_hom_inv' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
+    X ◁ f ≫ X ◁ inv f = 𝟙 (X ⊗ Y) := by
+  simp [← id_tensorHom, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem hom_inv_whiskerRight' {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
+    f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z) := by
+  simp [← tensorHom_id, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem whiskerLeft_inv_hom' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
+    X ◁ inv f ≫ X ◁ f = 𝟙 (X ⊗ Z) := by
+  simp [← id_tensorHom, ← tensor_comp]
+
+@[reassoc (attr := simp)]
+theorem inv_hom_whiskerRight' {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
+    inv f ▷ Z ≫ f ▷ Z = 𝟙 (Y ⊗ Z) := by
+  simp [← tensorHom_id, ← tensor_comp]
+
+/-- The left whiskering of an isomorphism is an isomorphism. -/
+@[simps]
+def whiskerLeftIso (X : C) {Y Z : C} (f : Y ≅ Z) : X ⊗ Y ≅ X ⊗ Z where
+  hom := X ◁ f.hom
+  inv := X ◁ f.inv
+
+instance whiskerLeft_isIso (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] : IsIso (X ◁ f) :=
+  IsIso.of_iso (whiskerLeftIso X (asIso f))
+
+@[simp]
+theorem inv_whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
+    inv (X ◁ f) = X ◁ inv f := by
+  aesop_cat
+
+/-- The right whiskering of an isomorphism is an isomorphism. -/
+@[simps!]
+def whiskerRightIso {X Y : C} (f : X ≅ Y) (Z : C) : X ⊗ Z ≅ Y ⊗ Z where
+  hom := f.hom ▷ Z
+  inv := f.inv ▷ Z
+
+instance whiskerRight_isIso {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] : IsIso (f ▷ Z) :=
+  IsIso.of_iso (whiskerRightIso (asIso f) Z)
+
+@[simp]
+theorem inv_whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) [IsIso f] :
+    inv (f ▷ Z) = inv f ▷ Z := by
+  aesop_cat
+
+end MonoidalCategory
 
 /-- The tensor product of two isomorphisms is an isomorphism. -/
 @[simps]
diff --git a/Mathlib/CategoryTheory/Monoidal/Center.lean b/Mathlib/CategoryTheory/Monoidal/Center.lean
@@ -248,6 +248,14 @@ theorem tensor_β (X Y : Center C) (U : C) :
   rfl
 #align category_theory.center.tensor_β CategoryTheory.Center.tensor_β
 
+@[simp]
+theorem whiskerLeft_f (X : Center C) {Y₁ Y₂ : Center C} (f : Y₁ ⟶ Y₂) : (X ◁ f).f = X.1 ◁ f.f :=
+  id_tensorHom X.1 f.f
+
+@[simp]
+theorem whiskerRight_f {X₁ X₂ : Center C} (f : X₁ ⟶ X₂) (Y : Center C) : (f ▷ Y).f = f.f ▷ Y.1 :=
+  tensorHom_id f.f Y.1
+
 @[simp]
 theorem tensor_f {X₁ Y₁ X₂ Y₂ : Center C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : (f ⊗ g).f = f.f ⊗ g.f :=
   rfl
@@ -337,12 +345,7 @@ open BraidedCategory
 /-- Auxiliary construction for `ofBraided`. -/
 @[simps]
 def ofBraidedObj (X : C) : Center C :=
-  ⟨X, {
-      β := fun Y => β_ X Y
-      monoidal := fun U U' => by
-        rw [Iso.eq_inv_comp, ← Category.assoc, ← Category.assoc, Iso.eq_comp_inv, Category.assoc,
-          Category.assoc]
-        exact hexagon_forward X U U' }⟩
+  ⟨X, { β := fun Y => β_ X Y}⟩
 #align category_theory.center.of_braided_obj CategoryTheory.Center.ofBraidedObj
 
 variable (C)
diff --git a/Mathlib/CategoryTheory/Monoidal/Linear.lean b/Mathlib/CategoryTheory/Monoidal/Linear.lean
@@ -32,13 +32,13 @@ variable [MonoidalCategory C]
 /-- A category is `MonoidalLinear R` if tensoring is `R`-linear in both factors.
 -/
 class MonoidalLinear [MonoidalPreadditive C] : Prop where
-  tensor_smul : ∀ {W X Y Z : C} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g) := by
+  whiskerLeft_smul : ∀ (X : C) {Y Z : C} (r : R) (f : Y ⟶ Z) , 𝟙 X ⊗ (r • f) = r • (𝟙 X ⊗ f) := by
     aesop_cat
-  smul_tensor : ∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g) := by
+  smul_whiskerRight : ∀ (r : R) {Y Z : C} (f : Y ⟶ Z) (X : C), (r • f) ⊗ 𝟙 X = r • (f ⊗ 𝟙 X) := by
     aesop_cat
 #align category_theory.monoidal_linear CategoryTheory.MonoidalLinear
 
-attribute [simp] MonoidalLinear.tensor_smul MonoidalLinear.smul_tensor
+attribute [simp] MonoidalLinear.whiskerLeft_smul MonoidalLinear.smul_whiskerRight
 
 variable {C}
 variable [MonoidalPreadditive C] [MonoidalLinear R C]
@@ -60,16 +60,16 @@ ensures that the domain is linear monoidal. -/
 theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
     [MonoidalCategory D] [MonoidalPreadditive D] (F : MonoidalFunctor D C) [Faithful F.toFunctor]
     [F.toFunctor.Additive] [F.toFunctor.Linear R] : MonoidalLinear R D :=
-  { tensor_smul := by
-      intros W X Y Z f r g
+  { whiskerLeft_smul := by
+      intros X Y Z r f
       apply F.toFunctor.map_injective
-      simp only [F.toFunctor.map_smul r (f ⊗ g), F.toFunctor.map_smul r g, F.map_tensor,
-        MonoidalLinear.tensor_smul, Linear.smul_comp, Linear.comp_smul]
-    smul_tensor := by
-      intros W X Y Z r f g
+      rw [F.map_whiskerLeft]
+      simp
+    smul_whiskerRight := by
+      intros r X Y f Z
       apply F.toFunctor.map_injective
-      simp only [F.toFunctor.map_smul r (f ⊗ g), F.toFunctor.map_smul r f, F.map_tensor,
-        MonoidalLinear.smul_tensor, Linear.smul_comp, Linear.comp_smul] }
+      rw [F.map_whiskerRight]
+      simp }
 #align category_theory.monoidal_linear_of_faithful CategoryTheory.monoidalLinearOfFaithful
 
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean b/Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean
@@ -82,6 +82,14 @@ theorem tensorHom {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : f ⊗ g = Limits.p
   rfl
 #align category_theory.monoidal_of_has_finite_products.tensor_hom CategoryTheory.monoidalOfHasFiniteProducts.tensorHom
 
+@[simp]
+theorem whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) : X ◁ f = Limits.prod.map (𝟙 X) f :=
+  rfl
+
+@[simp]
+theorem whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) : f ▷ Z = Limits.prod.map f (𝟙 Z) :=
+  rfl
+
 @[simp]
 theorem leftUnitor_hom (X : C) : (λ_ X).hom = Limits.prod.snd :=
   rfl
@@ -179,6 +187,14 @@ theorem tensorHom {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) : f ⊗ g = Limits.c
   rfl
 #align category_theory.monoidal_of_has_finite_coproducts.tensor_hom CategoryTheory.monoidalOfHasFiniteCoproducts.tensorHom
 
+@[simp]
+theorem whiskerLeft (X : C) {Y Z : C} (f : Y ⟶ Z) : X ◁ f = Limits.coprod.map (𝟙 X) f :=
+  rfl
+
+@[simp]
+theorem whiskerRight {X Y : C} (f : X ⟶ Y) (Z : C) : f ▷ Z = Limits.coprod.map f (𝟙 Z) :=
+  rfl
+
 @[simp]
 theorem leftUnitor_hom (X : C) : (λ_ X).hom = coprod.desc (initial.to X) (𝟙 _) :=
   rfl
diff --git a/Mathlib/Tactic/CategoryTheory/Coherence.lean b/Mathlib/Tactic/CategoryTheory/Coherence.lean
@@ -88,6 +88,14 @@ instance LiftHom_comp {X Y Z : C} [LiftObj X] [LiftObj Y] [LiftObj Z] (f : X ⟶
     [LiftHom f] [LiftHom g] : LiftHom (f ≫ g) where
   lift := LiftHom.lift f ≫ LiftHom.lift g
 
+instance liftHom_WhiskerLeft (X : C) [LiftObj X] {Y Z : C} [LiftObj Y] [LiftObj Z]
+    (f : Y ⟶ Z) [LiftHom f] : LiftHom (X ◁ f) where
+  lift := LiftObj.lift X ◁ LiftHom.lift f
+
+instance liftHom_WhiskerRight {X Y : C} (f : X ⟶ Y) [LiftObj X] [LiftObj Y] [LiftHom f]
+    {Z : C} [LiftObj Z] : LiftHom (f ▷ Z) where
+  lift := LiftHom.lift f ▷ LiftObj.lift Z
+
 instance LiftHom_tensor {W X Y Z : C} [LiftObj W] [LiftObj X] [LiftObj Y] [LiftObj Z]
     (f : W ⟶ X) (g : Y ⟶ Z) [LiftHom f] [LiftHom g] : LiftHom (f ⊗ g) where
   lift := LiftHom.lift f ⊗ LiftHom.lift g
@@ -109,19 +117,24 @@ namespace MonoidalCoherence
 instance refl (X : C) [LiftObj X] : MonoidalCoherence X X := ⟨𝟙 _⟩
 
 @[simps]
-instance tensor (X Y Z : C) [LiftObj X] [LiftObj Y] [LiftObj Z] [MonoidalCoherence Y Z] :
+instance whiskerLeft (X Y Z : C) [LiftObj X] [LiftObj Y] [LiftObj Z] [MonoidalCoherence Y Z] :
     MonoidalCoherence (X ⊗ Y) (X ⊗ Z) :=
   ⟨𝟙 X ⊗ MonoidalCoherence.hom⟩
 
+@[simps]
+instance whiskerRight (X Y Z : C) [LiftObj X] [LiftObj Y] [LiftObj Z] [MonoidalCoherence X Y] :
+    MonoidalCoherence (X ⊗ Z) (Y ⊗ Z) :=
+  ⟨MonoidalCoherence.hom ⊗ 𝟙 Z⟩
+
 @[simps]
 instance tensor_right (X Y : C) [LiftObj X] [LiftObj Y] [MonoidalCoherence (𝟙_ C) Y] :
     MonoidalCoherence X (X ⊗ Y) :=
-  ⟨(ρ_ X).inv ≫ (𝟙 X ⊗ MonoidalCoherence.hom)⟩
+  ⟨(ρ_ X).inv ≫ (X ◁  MonoidalCoherence.hom)⟩
 
 @[simps]
 instance tensor_right' (X Y : C) [LiftObj X] [LiftObj Y] [MonoidalCoherence Y (𝟙_ C)] :
     MonoidalCoherence (X ⊗ Y) X :=
-  ⟨(𝟙 X ⊗ MonoidalCoherence.hom) ≫ (ρ_ X).hom⟩
+  ⟨(X ◁ MonoidalCoherence.hom) ≫ (ρ_ X).hom⟩
 
 @[simps]
 instance left (X Y : C) [LiftObj X] [LiftObj Y] [MonoidalCoherence X Y] :
@@ -199,7 +212,7 @@ example {W X Y Z : C} (f : W ⟶ (X ⊗ Y) ⊗ Z) : W ⟶ X ⊗ (Y ⊗ Z) := f 
 
 example {U V W X Y : C} (f : U ⟶ V ⊗ (W ⊗ X)) (g : (V ⊗ W) ⊗ X ⟶ Y) :
     f ⊗≫ g = f ≫ (α_ _ _ _).inv ≫ g := by
-  simp [monoidalComp]
+  simp [MonoidalCategory.tensorHom_def, monoidalComp]
 
 end lifting
 
@@ -227,7 +240,7 @@ def mkProjectMapExpr (e : Expr) : TermElabM Expr := do
 /-- Coherence tactic for monoidal categories. -/
 def monoidal_coherence (g : MVarId) : TermElabM Unit := g.withContext do
   withOptions (fun opts => synthInstance.maxSize.set opts
-    (max 256 (synthInstance.maxSize.get opts))) do
+    (max 512 (synthInstance.maxSize.get opts))) do
   -- TODO: is this `dsimp only` step necessary? It doesn't appear to be in the tests below.
   let (ty, _) ← dsimp (← g.getType) (← Simp.Context.ofNames [] true)
   let some (_, lhs, rhs) := (← whnfR ty).eq? | exception g "Not an equation of morphisms."
