perf(CategoryTheory/Monoidal): change notations for tensor product of (iso)morphisms (#25922)

Discussions in #22698 made apparent that overloading notations was having a performance hit.
We obtain a small performance boost simply by changing notation for the tensor product of morphisms in monoidal categories from `⊗` to `⊗ₘ`, and the tensor product of isomorphisms from `⊗` to `⊗ᵢ`.

Co-authored-by: Yaël Dillies <[email protected]>



Co-authored-by: Yaël Dillies <[email protected]>

Author: robin-carlier

Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

@@ -134,7 +134,7 @@ theorem tensorObj_comul (K L : CoalgCat R) :
   rfl
 
 theorem tensorHom_toLinearMap (f : M →ₗc[R] N) (g : P →ₗc[R] Q) :
-    (CoalgCat.ofHom f ⊗ CoalgCat.ofHom g).1.toLinearMap
+    (CoalgCat.ofHom f ⊗ₘ CoalgCat.ofHom g).1.toLinearMap
       = TensorProduct.map f.toLinearMap g.toLinearMap := rfl
 
 theorem associator_hom_toLinearMap :

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

@@ -175,7 +175,7 @@ namespace MonoidalCategory
 
 @[simp]
 theorem tensorHom_tmul {K L M N : ModuleCat.{u} R} (f : K ⟶ L) (g : M ⟶ N) (k : K) (m : M) :
-    (f ⊗ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=
+    (f ⊗ₘ g) (k ⊗ₜ m) = f k ⊗ₜ g m :=
   rfl
 
 @[simp]

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

@@ -28,7 +28,7 @@ namespace MonoidalCategory
 
 @[simp]
 theorem braiding_naturality {X₁ X₂ Y₁ Y₂ : ModuleCat.{u} R} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) :
-    (f ⊗ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ f) := by
+    (f ⊗ₘ g) ≫ (Y₁.braiding Y₂).hom = (X₁.braiding X₂).hom ≫ (g ⊗ₘ f) := by
   ext : 1
   apply TensorProduct.ext'
   intro x y

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

@@ -72,7 +72,7 @@ lemma tensorObj_map_tmul {X Y : Cᵒᵖ} (f : X ⟶ Y) (m₁ : M₁.obj X) (m₂
 /-- The tensor product of two morphisms of presheaves of modules. -/
 @[simps]
 noncomputable def tensorHom (f : M₁ ⟶ M₂) (g : M₃ ⟶ M₄) : tensorObj M₁ M₃ ⟶ tensorObj M₂ M₄ where
-  app X := f.app X ⊗ g.app X
+  app X := f.app X ⊗ₘ g.app X
   naturality {X Y} φ := ModuleCat.MonoidalCategory.tensor_ext (fun m₁ m₃ ↦ by
     dsimp
     rw [tensorObj_map_tmul]

Mathlib/AlgebraicTopology/SimplicialSet/Monoidal.lean

@@ -47,7 +47,7 @@ lemma rightUnitor_inv_app_apply (K : SSet.{u}) {Δ : SimplexCategoryᵒᵖ} (x :
 @[simp]
 lemma tensorHom_app_apply {K K' L L' : SSet.{u}} (f : K ⟶ K') (g : L ⟶ L')
     {Δ : SimplexCategoryᵒᵖ} (x : (K ⊗ L).obj Δ) :
-    (f ⊗ g).app Δ x = ⟨f.app Δ x.1, g.app Δ x.2⟩ := rfl
+    (f ⊗ₘ g).app Δ x = ⟨f.app Δ x.1, g.app Δ x.2⟩ := rfl
 
 @[simp]
 lemma whiskerLeft_app_apply (K : SSet.{u}) {L L' : SSet.{u}} (g : L ⟶ L')

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -47,7 +47,7 @@ theorem tensorUnit_ρ {g : G} :
 
 @[simp]
 theorem tensor_ρ {X Y : Action V G} {g : G} :
-    @DFunLike.coe (G →* End (X.V ⊗ Y.V)) _ _ _ (X ⊗ Y).ρ g = X.ρ g ⊗ Y.ρ g :=
+    @DFunLike.coe (G →* End (X.V ⊗ Y.V)) _ _ _ (X ⊗ Y).ρ g = X.ρ g ⊗ₘ Y.ρ g :=
   rfl
 
 /-- Given an object `X` isomorphic to the tensor unit of `V`, `X` equipped with the trivial action

Mathlib/CategoryTheory/Closed/Cartesian.lean

@@ -242,7 +242,7 @@ theorem uncurry_pre (f : B ⟶ A) [Exponentiable B] (X : C) :
 
 theorem coev_app_comp_pre_app (f : B ⟶ A) [Exponentiable B] :
     (exp.coev A).app X ≫ (pre f).app (A ⊗ X) =
-      (exp.coev B).app X ≫ (exp B).map (f ⊗ 𝟙 _) := by
+      (exp.coev B).app X ≫ (exp B).map (f ⊗ₘ 𝟙 _) := by
   rw [tensorHom_id]
   exact unit_conjugateEquiv _ _ ((tensoringLeft _).map f) X
 

Mathlib/CategoryTheory/Closed/Functor.lean

@@ -153,7 +153,7 @@ theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) :
   unfold prodComparison
   have ηlemma : (h.unit.app (F.obj A ⊗ F.obj B) ≫
     lift ((L ⋙ F).map (fst _ _)) ((L ⋙ F).map (snd _ _))) =
-      (h.unit.app (F.obj A)) ⊗ (h.unit.app (F.obj B)) := by
+      (h.unit.app (F.obj A)) ⊗ₘ (h.unit.app (F.obj B)) := by
     ext <;> simp
   slice_lhs 1 2 => rw [ηlemma]
   simp only [Functor.id_obj, Functor.comp_obj, assoc, ← whisker_exchange, ← tensorHom_def']

Mathlib/CategoryTheory/Closed/Monoidal.lean

@@ -496,7 +496,7 @@ lemma curry'_ihom_map {X Y Z : C} [Closed X] (f : X ⟶ Y) (g : Y ⟶ Z) :
   simp only [curry', ← curry_natural_right, Category.assoc]
 
 lemma curry'_comp {X Y Z : C} [Closed X] [Closed Y] (f : X ⟶ Y) (g : Y ⟶ Z) :
-    curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ curry' g) ≫ comp X Y Z := by
+    curry' (f ≫ g) = (λ_ (𝟙_ C)).inv ≫ (curry' f ⊗ₘ curry' g) ≫ comp X Y Z := by
   rw [tensorHom_def_assoc, whiskerLeft_curry'_comp, MonoidalCategory.whiskerRight_id,
     Category.assoc, Category.assoc, Iso.inv_hom_id_assoc, ← unitors_equal,
     Iso.inv_hom_id_assoc, curry'_ihom_map]

Mathlib/CategoryTheory/Closed/Zero.lean

@@ -38,7 +38,7 @@ def uniqueHomsetOfInitialIsoUnit [HasInitial C] (i : ⊥_ C ≅ 𝟙_ C) (X Y :
   Equiv.unique <|
     calc
       (X ⟶ Y) ≃ (X ⊗ 𝟙_ C ⟶ Y) := Iso.homCongr (rightUnitor _).symm (Iso.refl _)
-      _ ≃ (X ⊗ ⊥_ C ⟶ Y) := (Iso.homCongr ((Iso.refl _) ⊗ i.symm) (Iso.refl _))
+      _ ≃ (X ⊗ ⊥_ C ⟶ Y) := (Iso.homCongr ((Iso.refl _) ⊗ᵢ i.symm) (Iso.refl _))
       _ ≃ (⊥_ C ⟶ Y ^^ X) := (exp.adjunction _).homEquiv _ _
 
 open scoped ZeroObject