English
There are symmetries exchanging the left and right positions in tensor products; explicit forms give leftComm and rightComm as canonical isomorphisms with symmetric behaviour.
Русский
Существуют симметрии, меняющие местами левый и правый множители в тензорном произведении; описанные лево- и право-симметрии являются каноническими изоморфизмами с симметричным поведением.
LaTeX
$$$\\text{leftComm} : M\\otimes_R N\\otimes_R P \\cong_R N\\otimes_R (M\\otimes_R P)$ and $\\text{rightComm} : M\\otimes_R N\\otimes_R P \\cong_R M\\otimes_R (P\\otimes_R N)$$$
Lean4
/-- This special case is worth defining explicitly since it is useful for defining multiplication
on tensor products of modules carrying multiplications (e.g., associative rings, Lie rings, ...).
E.g., suppose `M = P` and `N = Q` and that `M` and `N` carry bilinear multiplications:
`M ⊗ M → M` and `N ⊗ N → N`. Using `map`, we can define `(M ⊗ M) ⊗ (N ⊗ N) → M ⊗ N` which, when
combined with this definition, yields a bilinear multiplication on `M ⊗ N`:
`(M ⊗ N) ⊗ (M ⊗ N) → M ⊗ N`. In particular we could use this to define the multiplication in
the `TensorProduct.semiring` instance (currently defined "by hand" using `TensorProduct.mul`).
See also `mul_mul_mul_comm`. -/
def tensorTensorTensorComm : M ⊗[R] N ⊗[R] (P ⊗[R] Q) ≃ₗ[R] M ⊗[R] P ⊗[R] (N ⊗[R] Q) :=
(TensorProduct.assoc R (M ⊗[R] N) P Q).symm ≪≫ₗ congr (TensorProduct.rightComm R M N P) (.refl R Q) ≪≫ₗ
TensorProduct.assoc R (M ⊗[R] P) N Q
