Uncurrying alternating maps

Given a function f which is linear in the first argument and is alternating form in the other n arguments, this file defines an alternating form AlternatingMap.uncurryFin f in n + 1 arguments.

This function is given by

AlternatingMap.uncurryFin f v = ∑ i : Fin (n + 1), (-1) ^ (i : ℕ) • f (v i) (removeNth i v)

Given an alternating map f of n + 1 arguments, each term in the sum above written for f.curryLeft equals the original map, thus f.curryLeft.uncurryFin = (n + 1) • f.

We do not multiply the result of uncurryFin by (n + 1)⁻¹ so that the construction works for R-multilinear maps over any commutative ring R, not only a field of characteristic zero.

Main results

• AlternatingMap.uncurryFin_curryLeft: the round-trip formula for currying/uncurrying, see above.

• AlternatingMap.uncurryFin_uncurryFinLM_comp_of_symmetric: If f is a symmetric bilinear map taking values in the space of alternating maps, then the twice uncurried f is zero.

A version of the latter theorem for continuous alternating maps will be used to prove that the second exterior derivative of a differential form is zero.

theorem AlternatingMap.map_insertNth {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N) (p : Fin (n + 1)) (x : M) (v : Fin n → M) : f (p.insertNth x v) = (-1) ^ ↑p • f (Matrix.vecCons x v)

If f is a (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.

theorem AlternatingMap.neg_one_pow_smul_map_insertNth {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N) (p : Fin (n + 1)) (x : M) (v : Fin n → M) : (-1) ^ ↑p • f (p.insertNth x v) = f (Matrix.vecCons x v)

theorem AlternatingMap.neg_one_pow_smul_map_removeNth_add_eq_zero_of_eq {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n]→ₗ[R] N) {v : Fin (n + 1) → M} {i j : Fin (n + 1)} (hvij : v i = v j) (hij : i ≠ j) : (-1) ^ ↑i • f (i.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

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 uncurryFin below.

def AlternatingMap.uncurryFin {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : M [⋀^Fin (n + 1)]→ₗ[R] N

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

uncurryFin 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.

Equations

• AlternatingMap.uncurryFin f = { toMultilinearMap := ∑ p : Fin (n + 1), (-1) ^ ↑p • LinearMap.uncurryMid p (AlternatingMap.toMultilinearMapLM ∘ₗ f), map_eq_zero_of_eq' := ⋯ }

theorem AlternatingMap.uncurryFin_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v : Fin (n + 1) → M) : (uncurryFin f) v = ∑ i : Fin (n + 1), (-1) ^ ↑i • (f (v i)) (i.removeNth v)

@[simp]

theorem AlternatingMap.uncurryFin_add {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f g : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : uncurryFin (f + g) = uncurryFin f + uncurryFin g

@[simp]

theorem AlternatingMap.uncurryFin_curryLeft {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin (n + 1)]→ₗ[R] N) : uncurryFin f.curryLeft = (n + 1) • f

@[simp]

theorem AlternatingMap.uncurryFin_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} {S : Type u_6} [Monoid S] [DistribMulAction S N] [SMulCommClass R S N] (c : S) (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : uncurryFin (c • f) = c • uncurryFin f

def AlternatingMap.uncurryFinLM {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} : (M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) →ₗ[R] M [⋀^Fin (n + 1)]→ₗ[R] N

AlternaringMap.uncurryFin as a linear map.

Equations

• AlternatingMap.uncurryFinLM = { toFun := AlternatingMap.uncurryFin, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AlternatingMap.uncurryFinLM_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} (f : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N) : uncurryFinLM f = uncurryFin f

theorem AlternatingMap.uncurryFin_uncurryFinLM_comp_of_symmetric {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommRing R] [AddCommGroup M] [AddCommGroup N] [Module R M] [Module R N] {n : ℕ} {f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N} (hf : ∀ (x y : M), (f x) y = (f y) x) : uncurryFin (uncurryFinLM ∘ₗ f) = 0

If f is a symmetric bilinear map taking values in the space of alternating maps, then the twice uncurried f is zero.