English
Let f and g be bilinear maps giving a tensor product structure, and i1, i2, j1, j2 be linear maps between the corresponding modules. Then the induced tensor-product map obtained by composing along the first level with the maps (i1, i2) after applying the tensor-product structure to (j1, j2) equals the single induced map with the composed first factors: hg.map hp i1 i2 ((hf.map hg j1 j2) x) = hf.map hp (i1 ∘ j1) (i2 ∘ j2) x for all x.
Русский
Пусть f и g задают двуолнuдное отображение, задающее тензорное произведение, и i1, i2, j1, j2 — линейные отображения между соответствующими модулями. Тогда отображение, получаемое на тензорном произведении последовательным применением (i1, i2) после применения (j1, j2), равно отображению, получаемому непосредственным композиционным применением композиции (i1 ∘ j1, i2 ∘ j2) к исходному элементу: hg.map hp i1 i2 ((hf.map hg j1 j2) x) = hf.map hp (i1 ∘ j1) (i2 ∘ j2) x для всех x.
LaTeX
$$$ \forall x, \; hg.map hp i_1 i_2\big((hf.map hg j_1 j_2)\,x\big) = hf.map hp\big(i_1 \circ j_1\big)\big(i_2 \circ j_2\big)\,x $$$
Lean4
theorem map_map (x : M) : hg.map hp i₁ i₂ ((hf.map hg j₁ j₂) x) = hf.map hp (i₁ ∘ₗ j₁) (i₂ ∘ₗ j₂) x :=
DFunLike.congr_fun (hf.map_comp hg hp i₁ j₁ i₂ j₂).symm x
