map_comp — Mathlib

English

For families of linear maps f_i : s_i → t_i and g_i : t_i → t'_i, the induced map on the tensor product satisfies functoriality with respect to composition: map (i ↦ g_i ∘ f_i) = (map g) ∘ (map f).

Русский

Для семейств отображений f_i: s_i → t_i и g_i: t_i → t'_i отображение на тензорном произведении удовлетворяет формуле композиции: map (g_i ∘ f_i) = map g ∘ map f.

LaTeX

$$$\mathrm{map}(\lambda i, g_i \circ f_i) = (\mathrm{map}\ g) \circ (\mathrm{map}\ f)$$$

Lean4

theorem map_comp : map (fun (i : ι) ↦ g i ∘ₗ f i) = map g ∘ₗ map f :=
  by
  ext
  simp only [LinearMap.compMultilinearMap_apply, map_tprod, LinearMap.coe_comp, Function.comp_apply]

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