English
Let f: M → P and g: N → Q be linear maps, g': S → N, and x ∈ M ⊗_R S. Then applying g' on the second tensor factor before tensoring with f and g is the same as tensoring with g'∘g on the second factor after applying the map on the first component; i.e. TensorProduct.map f g (lTensor M g' x) = TensorProduct.map f (g ∘ g') x.
Русский
Пусть f: M → P и g: N → Q — линейные отображения, g': S → N и x ∈ M ⊗_R S. Тогда применение g' к второму фактору перед тензорированием с f и g эквивалентно тензорированию с g'∘g после применения отображения на первой компоненте; тождество TensorProduct.map f g (lTensor M g' x) = TensorProduct.map f (g ∘ g') x.
LaTeX
$$$$ \text{TensorProduct.map}\ f\ g\big((\mathrm{id}_M \otimes g')(x)\big) = \text{TensorProduct.map}\ f\ (g\circ g')\, x. $$$$
Lean4
@[simp]
theorem map_lTensor (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (g' : S →ₗ[R] N) (x : M ⊗[R] S) :
map f g (g'.lTensor M x) = map f (g ∘ₗ g') x :=
LinearMap.congr_fun (map_comp_lTensor _ _ _ _) x
