English
Alternatization is a monoid homomorphism from ContinuousMultilinearMap to ContinuousAlternatingMap, defined by summing over all permutations with sign: Alternatization(f) = ∑_{σ} sign(σ) · f ∘ σ.
Русский
Чередование — гомоморф моноида от ContinuousMultilinearMap к ContinuousAlternatingMap, определяется суммой по всем перестановкам с учетом знака: Alternatization(f) = ∑_{σ} sign(σ) · f ∘ σ.
LaTeX
$$$$ \\text{alternatization}(f) = \\sum_{\\sigma \\in \\operatorname{Perm}(\\iota)} \\operatorname{sign}(\\sigma) \\cdot f \\circ σ. $$$$
Lean4
/-- Alternatization of a continuous multilinear map. -/
@[simps -isSimp apply_toContinuousMultilinearMap]
def alternatization : ContinuousMultilinearMap R (fun _ : ι => M) N →+ M [⋀^ι]→L[R] N
where
toFun
f :=
{ toContinuousMultilinearMap := ∑ σ : Equiv.Perm ι, Equiv.Perm.sign σ • f.domDomCongr σ
map_eq_zero_of_eq' := fun v i j hv hne => by
simpa [MultilinearMap.alternatization_apply] using f.1.alternatization.map_eq_zero_of_eq' v i j hv hne }
map_zero' := by ext; simp
map_add' _ _ := by ext; simp [Finset.sum_add_distrib]
