liftIsometry_comp_mapL — Mathlib

English

The mapL construction respects the identity maps: mapL (i ↦ identity on E_i) equals the identity on the tensor product.

Русский

Конструкция mapL сохраняет тождественный отображение: mapL (i ↦ id_{E_i}) = id_{⨂ i, E_i}.

LaTeX

$$$ \\mathrm{mapL}(\\lambda i, \\mathrm{id}_{E_i}) = \\mathrm{id}_{\\bigotimes i, E_i} $$$

Lean4

theorem liftIsometry_comp_mapL (h : ContinuousMultilinearMap 𝕜 E' F) :
    liftIsometry 𝕜 E' F h ∘L mapL f = liftIsometry 𝕜 E F (h.compContinuousLinearMap f) :=
  by
  apply ContinuousLinearMap.coe_injective
  ext
  simp only [ContinuousLinearMap.coe_comp, mapL_coe, LinearMap.compMultilinearMap_apply, LinearMap.coe_comp,
    ContinuousLinearMap.coe_coe, Function.comp_apply, map_tprod, liftIsometry_apply_apply, lift.tprod,
    ContinuousMultilinearMap.coe_coe, ContinuousMultilinearMap.compContinuousLinearMap_apply]

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