English
There is a B-linear equivalence between (M ⊗_A P) ⊗_R Q and M ⊗_A (P ⊗_R Q), realized by the heterobasic associator.
Русский
Существует би-линейное биективное отображение между (M ⊗_A P) ⊗_R Q и M ⊗_A (P ⊗_R Q), задаваемое ассоциатором в heterogeneous базисе.
LaTeX
$$$(M\otimes_A P)\otimes_R Q \cong_B M\otimes_A(P\otimes_R Q)$$$
Lean4
/-- Heterobasic version of `TensorProduct.assoc`:
`B`-linear equivalence between `(M ⊗[A] P) ⊗[R] Q` and `M ⊗[A] (P ⊗[R] Q)`.
Note this is especially useful with `A = R` (where it is a "more linear" version of
`TensorProduct.assoc`), or with `B = A`. -/
def assoc : (M ⊗[A] P) ⊗[R] Q ≃ₗ[B] M ⊗[A] (P ⊗[R] Q) :=
LinearEquiv.ofLinear (lift <| lift <| lcurry R A B P Q _ ∘ₗ mk A B M (P ⊗[R] Q))
(lift <| uncurry R A B P Q _ ∘ₗ curry (mk R B _ Q)) (by ext; rfl) (by ext; rfl)
