English
The canonical n-alternating map from the dual of M to the dual of the n-th exterior power is defined via the tensor-power construction and the dual of the tensor power.
Русский
Каноническое n-альтернированное отображение из двойственного пространства M в двойственное пространство ∧^n M определено через тензорное произведение и двойственное тензорное произведение.
LaTeX
$$$ alternatingMapToDual(R\, M\, n) : AlternatingMap\ R\ (Module.Dual R M)\ (Module.Dual R (⋀[R]^n M))\ (Fin n) = \text{defined by } toMultilinearMap := (toTensorPower R M n).dualMap \circ MultilinearMap.multilinearMapToDual R M n $$$
Lean4
@[simp]
theorem toTensorPower_apply_ιMulti {n : ℕ} (v : Fin n → M) :
toTensorPower R M n (ιMulti R n v) = ∑ σ : Perm (Fin n), Perm.sign σ • PiTensorProduct.tprod R (fun i ↦ v (σ i)) :=
by
dsimp [toTensorPower]
simp only [alternatingMapLinearEquiv_apply_ιMulti, MultilinearMap.alternatization_apply,
MultilinearMap.domDomCongr_apply]
