map — Mathlib

English

For f : i ↦ s_i → t_i, the map_tprod lemma asserts that applying map f to tprod_R x gives tprod_R of f_i(x_i).

Русский

Лемма map_tprod утверждает: применение map f к tprod_R x даёт tprod_R (i ↦ f_i(x_i)).

LaTeX

$$$ map_tprod(x) : map(f)(tprod_R x) = tprod_R (i \mapsto f_i(x_i)) $$$

Lean4

/-- Let `sᵢ` and `tᵢ` be two families of `R`-modules.
Let `f` be a family of `R`-linear maps between `sᵢ` and `tᵢ`, i.e. `f : Πᵢ sᵢ → tᵢ`,
then there is an induced map `⨂ᵢ sᵢ → ⨂ᵢ tᵢ` by `⨂ aᵢ ↦ ⨂ fᵢ aᵢ`.

This is `TensorProduct.map` for an arbitrary family of modules.
-/
def map : (⨂[R] i, s i) →ₗ[R] ⨂[R] i, t i :=
  lift <| (tprod R).compLinearMap f

Похожие утверждения