Uncurrying continuous alternating maps #
Given a continuous function f which is linear in the first argument
and is alternating form in the other n arguments,
this file defines a continuous alternating form ContinuousAlternatingMap.alternatizeUncurryFin f
in n + 1 arguments.
This function is given by
ContinuousAlternatingMap.alternatizeUncurryFin f v =
∑ i : Fin (n + 1), (-1) ^ (i : ℕ) • f (v i) (removeNth i v)
Given a continuous alternating map f of n + 1 arguments,
each term in the sum above written for f.curryLeft equals the original map,
thus f.curryLeft.alternatizeUncurryFin = (n + 1) • f.
We do not multiply the result of alternatizeUncurryFin by (n + 1)⁻¹
so that the construction works for 𝕜-multilinear maps over any normed field 𝕜,
not only a field of characteristic zero.
Main results #
ContinuousAlternatingMap.alternatizeUncurryFin_curryLeft: the round-trip formula for currying/uncurrying, see above.ContinuousAlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric: Iffis a symmetric bilinear map taking values in the space of continuous alternating maps, then the twice uncurriedfis zero.
The latter theorem will be used to prove that the second exterior derivative of a differential form is zero.
If f is a continuous (n + 1)-multilinear alternating map, x is an element of the domain,
and v is an n-vector, then the value of f at v with x inserted at the pth place
equals (-1) ^ p times the value of f at v with x prepended.
Let v be an (n + 1)-tuple with two equal elements v i = v j, i ≠ j.
Let w i (resp., w j) be the vector v with ith (resp., jth) element removed.
Then (-1) ^ i • f (w i) + (-1) ^ j • f (w j) = 0.
This follows from the fact that these two vectors differ by a permutation of sign (-1) ^ (i + j).
These are the only two nonzero terms in the proof of map_eq_zero_of_eq
in the definition of AlternatingMap.alternatizeUncurryFin.
AlternaringMap.alternatizeUncurryFin as a continuous linear map.
Equations
Instances For
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.
Equations
Instances For
If f is a symmetric continuous bilinear map
taking values in the space of continuous alternating maps,
then the twice uncurried f is zero.