English
There exists a canonical linear map from the tensor power of the dual M^⋆ to the dual of the tensor power of M, obtained by lifting a multilinear map into the dual context.
Русский
Существует каноническое линейное отображение из тензорной степени двойственного пространства M^⋆ в двойственное пространство тензорного произведения ⨂^n M, получаемое поднятием мультинейтрической карты.
LaTeX
$$$ \\text{multilinearMapToDual}: ⨂[R]^n (M^*) \\to (⨂[R]^n M)^* $$$
Lean4
/-- The canonical multilinear map from `n` copies of the dual of the module `M`
to the dual of `⨂[R]^n M`. -/
noncomputable def multilinearMapToDual :
MultilinearMap R (fun (_ : Fin n) ↦ Module.Dual R M) (Module.Dual R (⨂[R]^n M)) :=
have :
∀ (_ : DecidableEq (Fin n)) (f : Fin n → Module.Dual R M) (φ : Module.Dual R M) (i j : Fin n) (v : Fin n → M),
(Function.update f i φ) j (v j) = Function.update (fun j ↦ f j (v j)) i (φ (v i)) j :=
fun _ f φ i j v ↦ by
by_cases h : j = i
· subst h
simp only [Function.update_self]
· simp only [Function.update_of_ne h]
{ toFun := fun f ↦ PiTensorProduct.lift (MultilinearMap.compLinearMap (MultilinearMap.mkPiRing R (Fin n) 1) f)
map_update_add' := fun f i φ₁ φ₂ ↦ by
ext v
dsimp
simp only [lift.tprod, MultilinearMap.compLinearMap_apply, this, LinearMap.add_apply,
MultilinearMap.map_update_add]
map_update_smul' := fun f i a φ ↦ by
ext v
dsimp
simp only [lift.tprod, MultilinearMap.compLinearMap_apply, this, LinearMap.smul_apply,
MultilinearMap.map_update_smul]
dsimp }
