English
Alternatization is expressed via a sum over permutations of signed domDomCongr; coercion of that equality matches the MultilinearMap statement.
Русский
Alternatization задается суммой по перестановкам с знаками; приведение равенств согласуется с MultilinearMap.
LaTeX
$$$AlternatingMap.alternatization(m) = \\sum_{σ} sign(σ) · domDomCongr(σ) m$$$
Lean4
/-- Two alternating maps indexed by a `Fintype` are equal if they are equal when all arguments
are distinct basis vectors. -/
theorem ext_alternating {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Basis ι₁ R' N₁)
(h : ∀ v : ι → ι₁, Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) : f = g :=
by
refine AlternatingMap.coe_multilinearMap_injective (Basis.ext_multilinear (fun _ ↦ e) fun v => ?_)
by_cases hi : Function.Injective v
· exact h v hi
· have : ¬Function.Injective fun i => e (v i) := hi.imp Function.Injective.of_comp
rw [coe_multilinearMap, coe_multilinearMap, f.map_eq_zero_of_not_injective _ this,
g.map_eq_zero_of_not_injective _ this]
