English
For bilinear maps f and g, map₂ applied to simple tensors satisfies: map₂ f g (m ⊗ n) = map (f m) (g n).
Русский
Для билинейных отображений f и g, при применении map₂ к простым тензорам: map₂ f g (m ⊗ n) = map (f m) (g n).
LaTeX
$$$\\text{map}_2(f,g)(m\\otimes n) = \\text{map}(f m)(g n)$$$
Lean4
/-- This is a binary version of `TensorProduct.map`: Given a bilinear map `f : M ⟶ P ⟶ Q` and a
bilinear map `g : N ⟶ S ⟶ T`, if we think `f` and `g` as linear maps with two inputs, then
`map₂ f g` is a bilinear map taking two inputs `M ⊗ N → P ⊗ S → Q ⊗ S` defined by
`map₂ f g (m ⊗ n) (p ⊗ s) = f m p ⊗ g n s`.
Mathematically, `TensorProduct.map₂` is defined as the composition
`M ⊗ N -map→ Hom(P, Q) ⊗ Hom(S, T) -homTensorHomMap→ Hom(P ⊗ S, Q ⊗ T)`.
-/
def map₂ (f : M →ₗ[R] P →ₗ[R] Q) (g : N →ₗ[R] S →ₗ[R] T) : M ⊗[R] N →ₗ[R] P ⊗[R] S →ₗ[R] Q ⊗[R] T :=
homTensorHomMap R _ _ _ _ ∘ₗ map f g
