English
The left-tensor and right-tensor operations satisfy the associativity constraint with the usual tensor product associator: for any x: M →ₗ[R] N, lTensor P (rTensor Q x) ∘ₗ TensorProduct.assoc R P M Q = TensorProduct.assoc R P N Q ∘ₗ rTensor Q (lTensor P x).
Русский
Операторы left-tensor и right-tensor удовлетворяют ассоциативному соотношению через ассоциатор тензорного произведения: для любого x: M →ₗ[R] N выполняется лефт-тензорная композиция равна правой композиции через ассоциатор.
LaTeX
$$$ lTensor P (rTensor Q x) \\circ \\mathrm{TensorProduct.assoc} \\\\ x \\,:=\\; \\mathrm{lTensor}_P (\\mathrm{rTensor}_Q x) \circ \\mathrm{assoc}_{R P M Q} = \\mathrm{assoc}_{R P N Q} \\circ (\\mathrm{rTensor}_Q (\\mathrm{lTensor}_P x)). $$$
Lean4
theorem lTensor_rTensor_comp_assoc (x : M →ₗ[R] N) :
lTensor P (rTensor Q x) ∘ₗ TensorProduct.assoc R P M Q = TensorProduct.assoc R P N Q ∘ₗ rTensor Q (lTensor P x) :=
by simp_rw [rTensor, lTensor, map_map_comp_assoc_eq]
