English
The inverse associator sends m ⊗ (n ⊗ p) to (m ⊗ n) ⊗ p.
Русский
Обратный ассоциатор переводит m ⊗ (n ⊗ p) в (m ⊗ n) ⊗ p.
LaTeX
$$$\\big(\\text{assoc}_R(M,N,P)\\big)^{-1}(m\\otimes_R (n\\otimes_R p)) = (m\\otimes_R n)\\otimes_R p$$$
Lean4
/-- This special case is useful for describing the interplay between `dualTensorHomEquiv` and
composition of linear maps.
E.g., composition of linear maps gives a map `(M → N) ⊗ (N → P) → (M → P)`, and applying
`dual_tensor_hom_equiv.symm` to the three hom-modules gives a map
`(M.dual ⊗ N) ⊗ (N.dual ⊗ P) → (M.dual ⊗ P)`, which agrees with the application of `contractRight`
on `N ⊗ N.dual` after the suitable rebracketing.
-/
def tensorTensorTensorAssoc : M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] (N ⊗[R] P) ⊗[R] Q :=
(TensorProduct.assoc R (M ⊗[R] N) P Q).symm ≪≫ₗ congr (TensorProduct.assoc R M N P) (1 : Q ≃ₗ[R] Q)
