Currying alternating forms

In this file we define AlternatingMap.curryLeft which interprets an alternating map in n + 1 variables as a linear map in the 0th variable taking values in the alternating maps in n variables.

def AlternatingMap.curryLeft {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) : M →ₗ[R] M [⋀^Fin n]→ₗ[R] N

Given an alternating map f in n+1 variables, split the first variable to obtain a linear map into alternating maps in n variables, given by x ↦ (m ↦ f (Matrix.vecCons x m)). It can be thought of as a map $Hom(\bigwedge^{n+1} M, N) \to Hom(M, Hom(\bigwedge^n M, N))$.

This is MultilinearMap.curryLeft for AlternatingMap. See also AlternatingMap.curryLeftLinearMap.

@[simp]

theorem AlternatingMap.curryLeft_apply_toMultilinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M) : ↑(f.curryLeft m) = (↑f).curryLeft m

@[simp]

theorem AlternatingMap.curryLeft_apply_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (x : M) (v : Fin n → M) : (f.curryLeft x) v = f (Matrix.vecCons x v)

@[simp]

theorem AlternatingMap.curryLeft_zero {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} : curryLeft 0 = 0

@[simp]

theorem AlternatingMap.curryLeft_add {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f g : M [⋀^Fin n.succ]→ₗ[R] N) : (f + g).curryLeft = f.curryLeft + g.curryLeft

@[simp]

theorem AlternatingMap.curryLeft_smul {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (r : R) (f : M [⋀^Fin n.succ]→ₗ[R] N) : (r • f).curryLeft = r • f.curryLeft

def AlternatingMap.curryLeftLinearMap {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} : M [⋀^Fin n.succ]→ₗ[R] N →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N

AlternatingMap.curryLeft as a LinearMap. This is a separate definition as dot notation does not work for this version.

@[simp]

theorem AlternatingMap.curryLeftLinearMap_apply {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) : curryLeftLinearMap f = f.curryLeft

@[simp]

theorem AlternatingMap.curryLeft_same {R : Type u_1} {M : Type u_2} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {n : ℕ} (f : M [⋀^Fin n.succ.succ]→ₗ[R] N) (m : M) : (f.curryLeft m).curryLeft m = 0

Currying with the same element twice gives the zero map.

@[simp]

theorem AlternatingMap.curryLeft_compAlternatingMap {R : Type u_1} {M : Type u_2} {N : Type u_4} {N₂ : Type u_5} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid N₂] [Module R M] [Module R N] [Module R N₂] {n : ℕ} (g : N →ₗ[R] N₂) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M) : (g.compAlternatingMap f).curryLeft m = g.compAlternatingMap (f.curryLeft m)

@[simp]

theorem AlternatingMap.curryLeft_compLinearMap {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M] [Module R M₂] [Module R N] {n : ℕ} (g : M₂ →ₗ[R] M) (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : M₂) : (f.compLinearMap g).curryLeft m = (f.curryLeft (g m)).compLinearMap g