map_comp_reindex_eq — Mathlib

English

Commutation of PiTensorProduct.map with reindexing up to an equivalent pullback map.

Русский

Коммутирование PiTensorProduct.map с переиндексацией до эквивалентного вытягивания обратно карты.

LaTeX

$$$\\operatorname{map} (\\lambda i. f_i) \\circ \\operatorname{reindex}_{R,s,e} = \\operatorname{reindex}_{R,t,e} \\circ \\operatorname{map} f$$$

Lean4

/-- Re-indexing the components of the tensor product by an equivalence `e` is compatible
with `PiTensorProduct.map`. -/
theorem map_comp_reindex_eq (f : Π i, s i →ₗ[R] t i) (e : ι ≃ ι₂) :
    map (fun i ↦ f (e.symm i)) ∘ₗ reindex R s e = reindex R t e ∘ₗ map f :=
  by
  ext m
  simp only [LinearMap.compMultilinearMap_apply, LinearEquiv.coe_coe, LinearMap.comp_apply, reindex_tprod, map_tprod]

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