Tensor product associator compatibility

This file restores an upstream tensor-product associator over mixed scalar towers.

def Algebra.TensorProduct.assoc' (R : Type u_1) (S : Type u_2) (R' : Type u_3) (A : Type u_4) (B : Type u_5) (C : Type u_6) [CommSemiring R] [CommSemiring S] [CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A] [Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C] [IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S] [IsScalarTower R' S A] [IsScalarTower R S A] : TensorProduct R (TensorProduct R' A B) C ≃ₐ[S] TensorProduct R' A (TensorProduct R B C)

An algebra equivalence reassociating tensor products over two scalar towers.

Equations

• Algebra.TensorProduct.assoc' R S R' A B C = AlgEquiv.ofLinearEquiv (TensorProduct.AlgebraTensorModule.assoc R R' S A B C) ⋯ ⋯

@[simp]

theorem Algebra.TensorProduct.assoc'_apply (R : Type u_1) (S : Type u_2) (R' : Type u_3) (A : Type u_4) (B : Type u_5) (C : Type u_6) [CommSemiring R] [CommSemiring S] [CommSemiring R'] [Semiring A] [Semiring B] [Semiring C] [Algebra R R'] [Algebra R A] [Algebra R' A] [Algebra R B] [Algebra R' B] [Algebra R C] [IsScalarTower R R' A] [IsScalarTower R R' B] [Algebra S A] [Algebra R S] [Algebra R' S] [IsScalarTower R' S A] [IsScalarTower R S A] (a : A) (b : B) (c : C) : (assoc' R S R' A B C) (a ⊗ₜ[R'] b ⊗ₜ[R] c) = a ⊗ₜ[R'] (b ⊗ₜ[R] c)