English
Given a linear map f that is linear in its first argument and alternating in the remaining n arguments, one constructs an alternating form in n+1 arguments by summing over Fin(n+1) with signs, i.e., alternatizeUncurryFin f(v) = sum_{i=Fin(n+1)} (-1)^{i} • f(v_i) (removeNth i v).
Русский
Дано линейное отображение f, линейное по первому аргументу и чередующееся по остальным n аргументам; строится чередующаяся форма в n+1 аргументов: alternatizeUncurryFin f(v) = сумма по i из Fin(n+1) с (-1)^i, применяя f к v_i и removeNth i v.
LaTeX
$$$ alternatizeUncurryFin : (M \to_{\!R} M [⋀^{\mathrm{Fin}\ n}]\to_{\!R} N) \to M [⋀^{\mathrm{Fin}\ (n+1)}] \to_{\!R} N $ \\ \\ alt(v) = \sum_{p: \mathrm{Fin}(n+1)} (-1)^{p} \cdot f(v_p) (p.removeNth v)$$
Lean4
/-- Given a function which is linear in the first argument
and is alternating in the other `n` arguments,
build an alternating form in `n + 1` arguments.
The function is given by
```
alternatizeUncurryFin f v = ∑ i : Fin (n + 1), (-1) ^ (i : ℕ) • f (v i) (removeNth i v)
```
Note that the round-trip with `curryFin` multiplies the form by `n + 1`,
since we want to avoid division in this definition. -/
def alternatizeUncurryFin (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : M [⋀^Fin (n + 1)]→ₗ[R] N
where
toMultilinearMap := ∑ p : Fin (n + 1), (-1) ^ (p : ℕ) • LinearMap.uncurryMid p (toMultilinearMapLM ∘ₗ f)
map_eq_zero_of_eq' := by
intro v i j hvij hij
suffices ∑ k : Fin (n + 1), (-1) ^ (k : ℕ) • f (v k) (k.removeNth v) = 0 by simpa
calc
_ = (-1) ^ (i : ℕ) • f (v i) (i.removeNth v) + (-1) ^ (j : ℕ) • f (v j) (j.removeNth v) :=
by
refine Fintype.sum_eq_add _ _ hij fun k ⟨hki, hkj⟩ ↦ ?_
rcases exists_succAbove_eq hki.symm with ⟨i, rfl⟩
rcases exists_succAbove_eq hkj.symm with ⟨j, rfl⟩
rw [(f (v k)).map_eq_zero_of_eq _ hvij (ne_of_apply_ne _ hij), smul_zero]
_ = 0 := by rw [hvij, neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq] <;> assumption
