The pairing between the tensor power of the dual and the tensor power

We construct the pairing TensorPower.pairingDual : ⨂[R]^n (Module.Dual R M) →ₗ[R] (Module.Dual R (⨂[R]^n M)).

noncomputable def TensorPower.multilinearMapToDual (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : MultilinearMap R (fun (x : Fin n) => Module.Dual R M) (Module.Dual R (TensorPower R n M))

The canonical multilinear map from n copies of the dual of the module M to the dual of ⨂[R]^n M.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TensorPower.multilinearMapToDual_apply_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (f : Fin n → Module.Dual R M) (v : Fin n → M) : ((multilinearMapToDual R M n) f) ((PiTensorProduct.tprod R) v) = ∏ i : Fin n, (f i) (v i)

noncomputable def TensorPower.pairingDual (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : TensorPower R n (Module.Dual R M) →ₗ[R] Module.Dual R (TensorPower R n M)

The linear map from the tensor power of the dual to the dual of the tensor power.

Equations

• TensorPower.pairingDual R M n = PiTensorProduct.lift (TensorPower.multilinearMapToDual R M n)

@[simp]

theorem TensorPower.pairingDual_tprod_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {n : ℕ} (f : Fin n → Module.Dual R M) (v : Fin n → M) : ((pairingDual R M n) ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) v) = ∏ i : Fin n, (f i) (v i)