English
There is a canonical linear map that sends a multilinear map to an alternating map by summing over all index permutations with their signs: alternatization m = ∑σ sign(σ) · m.domDomCongr σ.
Русский
Существует каноничное линейное преобразование, переводящее мультинелярную карту в чередующуюся, суммируя по всем перестановкам индексов с их знаками: alternatization m = ∑σ sign(σ) · m.domDomCongr σ.
LaTeX
$$$\\operatorname{alternatization} : \\text{MultilinearMap} \\to^+ \\text{AlternatingMap} $ defined by $\\operatorname{alternatization}(m) = \\sum_{\\sigma} \\operatorname{sign}(σ) \\cdot m\\,\\mathrm{domDomCongr}(σ)$$$
Lean4
/-- Produce an `AlternatingMap` out of a `MultilinearMap`, by summing over all argument
permutations. -/
def alternatization : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N'
where
toFun
m :=
{
∑ σ : Perm ι,
Equiv.Perm.sign σ •
m.domDomCongr σ with
toFun := ⇑(∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ)
map_eq_zero_of_eq' := fun v i j hvij hij => alternization_map_eq_zero_of_eq_aux m v i j hij hvij }
map_add' a
b := by
ext
simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply, add_apply, smul_add,
Finset.sum_add_distrib, AlternatingMap.add_apply]
map_zero' := by
ext
simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply, zero_apply, smul_zero,
Finset.sum_const_zero, AlternatingMap.zero_apply]
