English
Given a continuous linear map that is linear in the first argument and alternating in the rest, we obtain a continuous alternating map in one more argument by summing over coordinates with alternating signs.
Русский
Пусть дано непрерывное линейное отображение, линейное по первому аргументу и чередующееся по остальным аргументам; тогда заданием через сумму по координатам с чередованием получается непрерывная чередующая форма на один аргумент больше.
LaTeX
$$$\\text{alternatizeUncurryFin} : (E \\to_L[\\mathbb{k}] E [⋀^Fin n] \\to_L[\\mathbb{k}] F) \\to (E [⋀^Fin (n+1)] \\to_L[\\mathbb{k}] F)$$$
Lean4
/-- Given a continuous function which is linear in the first argument
and is alternating in the other `n` arguments,
build a continuous 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 `curryLeft` multiplies the form by `n + 1`,
since we want to avoid division in this definition. -/
noncomputable def alternatizeUncurryFin (f : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F) : E [⋀^Fin (n + 1)]→L[𝕜] F :=
alternatizeUncurryFinCLM 𝕜 E F f
