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
: Iff
is a symmetric bilinear map taking values in the space of continuous alternating maps, then the twice uncurriedf
is 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 p
th 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 i
th (resp., j
th) 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.