English
A symmetric version of the compatibility of maps with associator: the symm relation holds with flipped bracketing.
Русский
Симметричная совместимость отображений и ассоциатора: равенство сохраняется при смене скобок.
LaTeX
$$$(f\\otimes g)\\otimes h \\circ\\alpha_{M,N,P}^{-1} = \\alpha_{Q,S,T}^{-1} \\circ (f\\otimes (g\\otimes h))$$$
Lean4
/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `M ⊗ (N ⊗ P)`
with `(M ⊗ N) ⊗ P` and `Q ⊗ (S ⊗ T)` with `(Q ⊗ S) ⊗ T`, then this lemma states that
`(f ⊗ g) ⊗ h = f ⊗ (g ⊗ h)`. -/
theorem map_map_comp_assoc_symm_eq (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
map (map f g) h ∘ₗ (TensorProduct.assoc R M N P).symm = (TensorProduct.assoc R Q S T).symm ∘ₗ map f (map g h) :=
ext <| LinearMap.ext fun _ => ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => rfl
