lift_reindex_symm — Mathlib

English

There is a canonical isomorphism that identifies the Pi-tensor product indexed by a sum with a tensor product of PiTensorProducts.

Русский

Существует каноническое изоморфизм между PiTensorProduct, индексированным суммой, и тензорным произведением PiTensorProduct.

LaTeX

$$$\\PiTensorProduct.R\\;\\text{tmulEquivDep} : (⨂[R] i, N(.inl i)) \\otimes_R (⨂[R] i, N(.inr i)) \\cong_R ⨂[R] i, N i$$$

Lean4

@[simp]
theorem lift_reindex_symm (e : ι ≃ ι₂) (φ : MultilinearMap R s E) (x : ⨂[R] i, s (e.symm i)) :
    lift φ (reindex R s e |>.symm x) = lift (domDomCongrLinearEquiv' R R s _ e φ) x :=
  LinearMap.congr_fun (lift_comp_reindex_symm e φ) x

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