Uncurrying alternating maps in the first argument

Mathlib's AlternatingMap.curryLeft turns an alternating map f in n + 2 arguments into a linear family x ↦ f.curryLeft x of alternating maps in n + 1 arguments, and every member of that family vanishes once its first argument is x again (AlternatingMap.curryLeft_same). This file constructs the inverse: a linear family g of alternating maps with (g x).curryLeft x = 0 for every x assembles into the alternating map AlternatingMap.uncurryLeft g hg with uncurryLeft g hg v = g (v 0) (Fin.tail v).

So an alternating map may be defined by giving its value with the first argument fixed, and checking only that it vanishes when the first two arguments agree. This is how the Chevalley–Eilenberg differential, defined degree by degree through its interior products, is shown to be alternating. The file also records that alternating maps are determined by their interior products (AlternatingMap.curryLeft_injective) and that interior products anticommute (AlternatingMap.curryLeft_curryLeft_eq_neg). If ι_x f = 0, then f vanishes on every family with x in some slot (AlternatingMap.map_eq_zero_of_curryLeft_eq_zero) and does not see the components of its arguments along x (AlternatingMap.map_add_smul_of_curryLeft_eq_zero): this is how a form whose contraction with a vector field vanishes descends along that field.

theorem AlternatingMap.curryLeft_injective {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] : Function.Injective curryLeft

An alternating map in at least one argument is determined by its interior products.

theorem AlternatingMap.curryLeft_curryLeft_eq_neg {R : Type u_1} {M : Type u_2} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Type u_4} [AddCommGroup N] [Module R N] (f : M [⋀^Fin (n + 2)]→ₗ[R] N) (x y : M) : (f.curryLeft x).curryLeft y = -(f.curryLeft y).curryLeft x

Interior products anticommute: exchanging the first two arguments changes the sign.

def AlternatingMap.uncurryLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] M [⋀^Fin (n + 1)]→ₗ[R] N) (hg : ∀ (x : M), (g x).curryLeft x = 0) : M [⋀^Fin (n + 2)]→ₗ[R] N

A linear family g of alternating maps in n + 1 arguments, each vanishing when its first argument equals the parameter, assembles into an alternating map in n + 2 arguments whose first argument is the parameter. This inverts AlternatingMap.curryLeft.

@[simp]

theorem AlternatingMap.uncurryLeft_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] M [⋀^Fin (n + 1)]→ₗ[R] N) (hg : ∀ (x : M), (g x).curryLeft x = 0) (v : Fin (n + 2) → M) : (uncurryLeft g hg) v = (g (v 0)) (Fin.tail v)

The first argument of uncurryLeft g hg selects the member of the family g.

@[simp]

theorem AlternatingMap.curryLeft_uncurryLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (g : M →ₗ[R] M [⋀^Fin (n + 1)]→ₗ[R] N) (hg : ∀ (x : M), (g x).curryLeft x = 0) : (uncurryLeft g hg).curryLeft = g

Currying uncurryLeft g hg recovers the family g.

@[simp]

theorem AlternatingMap.uncurryLeft_curryLeft {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M [⋀^Fin (n + 2)]→ₗ[R] N) : uncurryLeft f.curryLeft ⋯ = f

Uncurrying the interior products of f recovers f.

theorem AlternatingMap.map_eq_zero_of_curryLeft_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M [⋀^Fin (n + 1)]→ₗ[R] N} {x : M} (hx : f.curryLeft x = 0) {v : Fin (n + 1) → M} {j : Fin (n + 1)} (hv : v j = x) : f v = 0

If the interior product ι_x f vanishes, then f vanishes on every family of vectors with x in some slot, not only in the first one.

theorem AlternatingMap.map_add_smul_of_curryLeft_eq_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} {n : ℕ} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M [⋀^Fin (n + 1)]→ₗ[R] N} {x : M} (hx : f.curryLeft x = 0) (v : Fin (n + 1) → M) (a : Fin (n + 1) → R) : (f fun (i : Fin (n + 1)) => v i + a i • x) = f v

If the interior product ι_x f vanishes, then f does not see the components of its arguments along x: f (v₀ + a₀ x, …, vₙ + aₙ x) = f (v₀, …, vₙ).