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.alternatizeUncurryFin f in n + 1 arguments.

This function is given by

AlternatingMap.alternatizeUncurryFin 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.alternatizeUncurryFin = (n + 1) • f.

We do not multiply the result of alternatizeUncurryFin 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.alternatizeUncurryFin_curryLeft: the round-trip formula for currying/uncurrying, see above.

• AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_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 alternatizeUncurryFin below.

def AlternatingMap.alternatizeUncurryFin {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

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.

Equations

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

@[deprecated AlternatingMap.alternatizeUncurryFin (since := "2025-09-30")]

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

Alias of AlternatingMap.alternatizeUncurryFin.

---

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.

Equations

• @AlternatingMap.uncurryFin = @AlternatingMap.alternatizeUncurryFin

theorem AlternatingMap.alternatizeUncurryFin_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) : (alternatizeUncurryFin f) v = ∑ i : Fin (n + 1), (-1) ^ ↑i • (f (v i)) (i.removeNth v)

@[deprecated AlternatingMap.alternatizeUncurryFin_apply (since := "2025-09-30")]

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) : (alternatizeUncurryFin f) v = ∑ i : Fin (n + 1), (-1) ^ ↑i • (f (v i)) (i.removeNth v)

Alias of AlternatingMap.alternatizeUncurryFin_apply.

@[simp]

theorem AlternatingMap.alternatizeUncurryFin_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) : alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g

@[deprecated AlternatingMap.alternatizeUncurryFin_add (since := "2025-09-30")]

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) : alternatizeUncurryFin (f + g) = alternatizeUncurryFin f + alternatizeUncurryFin g

Alias of AlternatingMap.alternatizeUncurryFin_add.

@[simp]

theorem AlternatingMap.alternatizeUncurryFin_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) : alternatizeUncurryFin f.curryLeft = (n + 1) • f

@[deprecated AlternatingMap.alternatizeUncurryFin_curryLeft (since := "2025-09-30")]

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) : alternatizeUncurryFin f.curryLeft = (n + 1) • f

Alias of AlternatingMap.alternatizeUncurryFin_curryLeft.

@[simp]

theorem AlternatingMap.alternatizeUncurryFin_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) : alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f

@[deprecated AlternatingMap.alternatizeUncurryFin_smul (since := "2025-09-30")]

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) : alternatizeUncurryFin (c • f) = c • alternatizeUncurryFin f

Alias of AlternatingMap.alternatizeUncurryFin_smul.

def AlternatingMap.alternatizeUncurryFinLM {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

AlternatingMap.alternatizeUncurryFin as a linear map.

Equations

• AlternatingMap.alternatizeUncurryFinLM = { toFun := AlternatingMap.alternatizeUncurryFin, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem AlternatingMap.alternatizeUncurryFinLM_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) : alternatizeUncurryFinLM f = alternatizeUncurryFin f

@[deprecated AlternatingMap.alternatizeUncurryFinLM (since := "2025-09-30")]

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

Alias of AlternatingMap.alternatizeUncurryFinLM.

---

AlternatingMap.alternatizeUncurryFin as a linear map.

Equations

• @AlternatingMap.uncurryFinLM = @AlternatingMap.alternatizeUncurryFinLM

theorem AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_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 →ₗ[R] M [⋀^Fin n]→ₗ[R] N) (v : Fin (n + 2) → M) : (alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f)) v = ∑ i : Fin (n + 1), ∑ j ∈ Finset.Ici i, (-1) ^ (↑i + ↑j) • (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) - ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

If f is a bilinear map taking values in the space of alternating maps, then evaluation of the twice uncurried f on a tuple of vectors v can be represented as a sum of

$$ f(v_i, v_j; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}-) - f(v_j, v_i; v_0, \dots, \hat{v_i}, \dots, \hat{v_j}-) $$

over all (i j : Fin (n + 2)), i < j, taken with appropriate signs. Here $$\hat{v_i}$$ and $$\hat{v_j}$$ mean that these vectors are removed from the tuple.

We use pairs of i j : Fin (n + 1), i ≤ j, to encode pairs (i.castSucc : Fin (n + 1), j.succ : Fin (n + 1)), so the power of -1 is off by one compared to the informal texts.

In particular, if f is symmetric in the first two arguments, then the resulting alternating map is zero, see alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric below.

theorem AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_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) : alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) = 0

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

See also alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply for a formula that does not assume f to be symmetric.

@[deprecated AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_comp_of_symmetric (since := "2025-09-30")]

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) : alternatizeUncurryFin (alternatizeUncurryFinLM ∘ₗ f) = 0

Alias of AlternatingMap.alternatizeUncurryFin_alternatizeUncurryFinLM_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.

See also alternatizeUncurryFin_alternatizeUncurryFinLM_comp_apply for a formula that does not assume f to be symmetric.