lift_reindex — Mathlib

English

For x in the Pi tensor product, lifting after reindexing equals lifting after applying the pulled-back map to x.

Русский

Для x в Pi TensorProduct подъем после переиндексации равняется подъему после применения вытянутой карты к x.

LaTeX

$$$\\operatorname{lift} \\phi (\\operatorname{reindex}_{R,s,e} x) = \\operatorname{lift}(\\operatorname{domDomCongrLinearEquiv'}^{\\,-1}_{R,R,s,e} \\phi) (x).$$$

Lean4

theorem lift_reindex (e : ι ≃ ι₂) (φ : MultilinearMap R (fun i ↦ s (e.symm i)) E) (x : ⨂[R] i, s i) :
    lift φ (reindex R s e x) = lift ((domDomCongrLinearEquiv' R R s _ e).symm φ) x :=
  LinearMap.congr_fun (lift_comp_reindex e φ) x

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