chore(RingTheory/TensorProduct): make Algebra.TensorProduct.assoc more linear (leanprover-community#34947)

We also remove two unused `aux` lemmas that can be recovered by the multiplicative properties of `Algebra.TensorProduct.assoc`.

Author: chrisflav

Mathlib/Algebra/Category/AlgCat/Monoidal.lean

@@ -53,7 +53,7 @@ instance : MonoidalCategoryStruct (AlgCat.{u} R) where
   whiskerRight {X₁ X₂} (f : X₁ ⟶ X₂) Y := tensorHom f (𝟙 Y)
   tensorHom := tensorHom
   tensorUnit := of R R
-  associator X Y Z := (Algebra.TensorProduct.assoc R R X Y Z).toAlgebraIso
+  associator X Y Z := (Algebra.TensorProduct.assoc R R R X Y Z).toAlgebraIso
   leftUnitor X := (Algebra.TensorProduct.lid R X).toAlgebraIso
   rightUnitor X := (Algebra.TensorProduct.rid R R X).toAlgebraIso
 
@@ -86,11 +86,11 @@ theorem hom_inv_rightUnitor {M : AlgCat.{u} R} :
   rfl
 
 theorem hom_hom_associator {M N K : AlgCat.{u} R} :
-    (α_ M N K).hom.hom = (Algebra.TensorProduct.assoc R R M N K).toAlgHom :=
+    (α_ M N K).hom.hom = (Algebra.TensorProduct.assoc R R R M N K).toAlgHom :=
   rfl
 
 theorem hom_inv_associator {M N K : AlgCat.{u} R} :
-    (α_ M N K).inv.hom = (Algebra.TensorProduct.assoc R R M N K).symm.toAlgHom :=
+    (α_ M N K).inv.hom = (Algebra.TensorProduct.assoc R R R M N K).symm.toAlgHom :=
   rfl
 
 noncomputable instance instMonoidalCategory : MonoidalCategory (AlgCat.{u} R) :=

Mathlib/Algebra/Category/CommAlgCat/Monoidal.lean

@@ -58,7 +58,7 @@ instance : MonoidalCategory (CommAlgCat.{u} R) where
   whiskerRight f T := ofHom (map f.hom (.id _ _))
   tensorHom f g := ofHom (map f.hom g.hom)
   tensorUnit := .of R R
-  associator _ _ _ := isoMk (assoc R R _ _ _)
+  associator _ _ _ := isoMk (assoc R R R _ _ _)
   leftUnitor _ := isoMk (lid R _)
   rightUnitor _ := isoMk (rid R R _)
 
@@ -77,10 +77,10 @@ variable (C) in
 @[simp] lemma whiskerLeft_hom (f : A ⟶ B) : (C ◁ f).hom = map (.id _ _) f.hom := rfl
 
 variable (A B C) in
-@[simp] lemma associator_hom_hom : (α_ A B C).hom.hom = (assoc R R A B C).toAlgHom := rfl
+@[simp] lemma associator_hom_hom : (α_ A B C).hom.hom = (assoc R R R A B C).toAlgHom := rfl
 
 variable (A B C) in
-@[simp] lemma associator_inv_hom : (α_ A B C).inv.hom = (assoc R R A B C).symm.toAlgHom := rfl
+@[simp] lemma associator_inv_hom : (α_ A B C).inv.hom = (assoc R R R A B C).symm.toAlgHom := rfl
 
 instance : BraidedCategory (CommAlgCat.{u} R) where
   braiding S T := isoMk (comm R _ _)

Mathlib/RingTheory/Bialgebra/Basic.lean

@@ -177,7 +177,7 @@ then `Bialgebra.ofAlgHom` consumes the counit and comultiplication
 as algebra homomorphisms that satisfy the coalgebra axioms to define
 a bialgebra structure on `A`. -/
 abbrev ofAlgHom (comul : A →ₐ[R] (A ⊗[R] A)) (counit : A →ₐ[R] R)
-    (h_coassoc : (Algebra.TensorProduct.assoc R R A A A).toAlgHom.comp
+    (h_coassoc : (Algebra.TensorProduct.assoc R R R A A A).toAlgHom.comp
       ((Algebra.TensorProduct.map comul (.id R A)).comp comul)
       = (Algebra.TensorProduct.map (.id R A) comul).comp comul)
     (h_rTensor : (Algebra.TensorProduct.map counit (.id R A)).comp comul

Mathlib/RingTheory/Bialgebra/TensorProduct.lean

@@ -90,7 +90,7 @@ variable (R S A C D) in
 /-- The associator for tensor products of R-bialgebras, as a bialgebra equivalence. -/
 protected noncomputable def assoc :
     (A ⊗[S] C) ⊗[R] D ≃ₐc[S] A ⊗[S] (C ⊗[R] D) :=
-  { Coalgebra.TensorProduct.assoc R S A C D, Algebra.TensorProduct.assoc R S A C D with }
+  { Coalgebra.TensorProduct.assoc R S A C D, Algebra.TensorProduct.assoc R S S A C D with }
 
 @[simp]
 theorem assoc_tmul (x : A) (y : C) (z : D) :
@@ -110,7 +110,7 @@ theorem assoc_toCoalgEquiv :
 @[simp]
 theorem assoc_toAlgEquiv :
     (Bialgebra.TensorProduct.assoc R S A C D : _ ≃ₐ[S] _) =
-    Algebra.TensorProduct.assoc R S A C D := rfl
+    Algebra.TensorProduct.assoc R S S A C D := rfl
 
 variable (R B) in
 /-- The base ring is a left identity for the tensor product of bialgebras, up to

Mathlib/RingTheory/TensorProduct/Maps.lean

@@ -21,7 +21,7 @@ This file provides results about maps between tensor products of `R`-algebras.
   * `Algebra.TensorProduct.lid : R ⊗[R] A ≃ₐ[R] A`
   * `Algebra.TensorProduct.rid : A ⊗[R] R ≃ₐ[S] A` (usually used with `S = R` or `S = A`)
   * `Algebra.TensorProduct.comm : A ⊗[R] B ≃ₐ[R] B ⊗[R] A`
-  * `Algebra.TensorProduct.assoc : ((A ⊗[R] B) ⊗[R] C) ≃ₐ[R] (A ⊗[R] (B ⊗[R] C))`
+  * `Algebra.TensorProduct.assoc : ((A ⊗[S] C) ⊗[R] D) ≃ₐ[T] (A ⊗[S] (C ⊗[R] D))`
 - `Algebra.TensorProduct.liftEquiv`: a universal property for the tensor product of algebras.
 
 ## References
@@ -368,39 +368,28 @@ end
 
 section
 
-variable {R A}
-
-unseal mul in
-theorem assoc_aux_1 (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C) :
-    (TensorProduct.assoc R A B C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) =
-      (TensorProduct.assoc R A B C) (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) *
-        (TensorProduct.assoc R A B C) (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂) :=
-  rfl
-
-theorem assoc_aux_2 : (TensorProduct.assoc R A B C) (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1 :=
-  rfl
-
-variable (R A C D)
+variable [CommSemiring T] [Algebra R T] [Algebra S T]
+    [Algebra T A] [IsScalarTower R T A] [IsScalarTower S T A]
 
+variable (T C D) in
 /-- The associator for tensor product of R-algebras, as an algebra isomorphism. -/
-protected def assoc : A ⊗[S] C ⊗[R] D ≃ₐ[S] A ⊗[S] (C ⊗[R] D) :=
+protected def assoc : (A ⊗[S] C) ⊗[R] D ≃ₐ[T] A ⊗[S] (C ⊗[R] D) :=
   AlgEquiv.ofLinearEquiv
-    (AlgebraTensorModule.assoc R S S A C D)
+    (AlgebraTensorModule.assoc R S T A C D)
     (by simp [Algebra.TensorProduct.one_def])
     ((LinearMap.map_mul_iff _).mpr <| by ext; simp)
 
+variable (T C D) in
 @[simp] theorem assoc_toLinearEquiv :
-    (TensorProduct.assoc R S A C D).toLinearEquiv = AlgebraTensorModule.assoc R S S A C D := rfl
-
-variable {A C D}
+    (TensorProduct.assoc R S T A C D).toLinearEquiv = AlgebraTensorModule.assoc R S T A C D := rfl
 
 @[simp]
 theorem assoc_tmul (a : A) (b : C) (c : D) :
-    TensorProduct.assoc R S A C D ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) := rfl
+    TensorProduct.assoc R S T A C D ((a ⊗ₜ b) ⊗ₜ c) = a ⊗ₜ (b ⊗ₜ c) := rfl
 
 @[simp]
 theorem assoc_symm_tmul (a : A) (b : C) (c : D) :
-    (TensorProduct.assoc R S A C D).symm (a ⊗ₜ (b ⊗ₜ c)) = (a ⊗ₜ b) ⊗ₜ c := rfl
+    (TensorProduct.assoc R S T A C D).symm (a ⊗ₜ (b ⊗ₜ c)) = (a ⊗ₜ b) ⊗ₜ c := rfl
 
 end
 
@@ -541,8 +530,8 @@ variable (R A B C) in
 
 This is the algebra version of `TensorProduct.leftComm`. -/
 def leftComm : A ⊗[R] (B ⊗[R] C) ≃ₐ[R] B ⊗[R] (A ⊗[R] C) :=
-  (Algebra.TensorProduct.assoc R R A B C).symm.trans <|
-    (congr (Algebra.TensorProduct.comm R A B) .refl).trans <| TensorProduct.assoc R R B A C
+  (Algebra.TensorProduct.assoc R R R A B C).symm.trans <|
+    (congr (Algebra.TensorProduct.comm R A B) .refl).trans <| TensorProduct.assoc R R R B A C
 
 @[simp]
 theorem leftComm_tmul (m : A) (n : B) (p : C) :