English
Let f1: M → M2, g1: N → N2, f2: M2 → M3 and g2: N2 → N3 be linear maps, and x ∈ M ⊗_R N. Then applying the tensor-product map twice is the same as applying the composed maps once: map f2 g2 ( map f1 g1 x ) = map (f2 ∘ f1) (g2 ∘ g1) x.
Русский
Пусть f1: M → M2, g1: N → N2, f2: M2 → M3 и g2: N2 → N3 — линейные отображения, x ∈ M ⊗_R N. Тогда применение тензорного отображения два раза равно применению объединённых отображений: map f2 g2 ( map f1 g1 x ) = map (f2 ∘ f1) (g2 ∘ g1) x.
LaTeX
$$$\\operatorname{map} f_2 g_2\\bigl(\\operatorname{map} f_1 g_1(x)\\bigr) = \\operatorname{map} (f_2 \\circ f_1) (g_2 \\circ g_1) x$$$
Lean4
theorem map_map (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂) (x : M ⊗[R] N) :
map f₂ g₂ (map f₁ g₁ x) = map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) x :=
DFunLike.congr_fun (map_comp ..).symm x
