English
Let f_i : s_i → t_i → t'_i; then map₂ f on tprod x and tprod y yields tprod of the pointwise application f_i(x_i)(y_i).
Русский
Пусть f_i : s_i → t_i → t'_i; тогда map₂ f действует на tprod x и tprod y и даёт тензор, компоненты которого равны f_i(x_i)(y_i).
LaTeX
$$$\mathrm{map}_2\ f\ (\,tprod\ R x\ )\ (tprod\ R y) = tprod\ R (\lambda i. f_i(x_i)(y_i))$$$
Lean4
/-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an
element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.
This is `PiTensorProduct.map` for two arbitrary families of modules.
This is `TensorProduct.map₂` for families of modules.
-/
def map₂ (f : Π i, s i →ₗ[R] t i →ₗ[R] t' i) : (⨂[R] i, s i) →ₗ[R] (⨂[R] i, t i) →ₗ[R] ⨂[R] i, t' i :=
lift <| LinearMap.compMultilinearMap piTensorHomMap <| (tprod R).compLinearMap f
