English
Given linear maps f,g,h, the canonical diagram commutes: map maps respect associativity of triple tensor product; i.e. f ⊗ (g ⊗ h) equals (f ⊗ g) ⊗ h after applying the associator.
Русский
Даны линейные отображения f,g,h; каноническая диаграмма с ассоциатором commute: f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h после применения ассоциатора.
LaTeX
$$$(f\\otimes (g\\otimes h)) \\circ\\alpha_{M,N,P} = \\alpha_{Q,S,T} \\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_eq (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) :
map f (map g h) ∘ₗ TensorProduct.assoc R M N P = TensorProduct.assoc R Q S T ∘ₗ map (map f g) h :=
ext <| ext <| LinearMap.ext fun _ => LinearMap.ext fun _ => LinearMap.ext fun _ => rfl
