Currying of multilinear maps

We register isomorphisms corresponding to currying or uncurrying variables, transforming a multilinear function f on n+1 variables into a linear function taking values in multilinear functions in n variables, and into a multilinear function in n variables taking values in linear functions. These operations are called f.curryLeft and f.curryRight respectively (with inverses f.uncurryLeft and f.uncurryRight). These operations induce linear equivalences between spaces of multilinear functions in n+1 variables and spaces of linear functions into multilinear functions in n variables (resp. multilinear functions in n variables taking values in linear functions), called respectively multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

Currying

We associate to a multilinear map in n+1 variables (i.e., based on Fin n.succ) two curried functions, named f.curryLeft (which is a linear map on E 0 taking values in multilinear maps in n variables) and f.curryRight (which is a multilinear map in n variables taking values in linear maps on E 0). In both constructions, the variable that is singled out is 0, to take advantage of the operations cons and tail on Fin n. The inverse operations are called uncurryLeft and uncurryRight.

We also register linear equiv versions of these correspondences, in multilinearCurryLeftEquiv and multilinearCurryRightEquiv.

Left currying

def LinearMap.uncurryLeft {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂) : MultilinearMap R M M₂

Given a linear map f from M 0 to multilinear maps on n variables, construct the corresponding multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (m 0) (tail m)

Equations

• f.uncurryLeft = { toFun := fun (m : (i : Fin n.succ) → M i) => (f (m 0)) (Fin.tail m), map_update_add' := ⋯, map_update_smul' := ⋯ }

@[simp]

theorem LinearMap.uncurryLeft_apply {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂) (m : (i : Fin n.succ) → M i) : f.uncurryLeft m = (f (m 0)) (Fin.tail m)

def MultilinearMap.curryLeft {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂

Given a multilinear map f in n+1 variables, split the first variable to obtain a linear map into multilinear maps in n variables, given by x ↦ (m ↦ f (cons x m)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MultilinearMap.curryLeft_apply {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (x : M 0) (m : (i : Fin n) → M i.succ) : (f.curryLeft x) m = f (Fin.cons x m)

@[simp]

theorem LinearMap.curry_uncurryLeft {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂) : f.uncurryLeft.curryLeft = f

@[simp]

theorem MultilinearMap.uncurry_curryLeft {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) : f.curryLeft.uncurryLeft = f

def multilinearCurryLeftEquiv (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] : MultilinearMap R M M₂ ≃ₗ[R] M 0 →ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.succ) M₂

The space of multilinear maps on Π (i : Fin (n+1)), M i is canonically isomorphic to the space of linear maps from M 0 to the space of multilinear maps on Π (i : Fin n), M i.succ, by separating the first variable. We register this isomorphism as a linear isomorphism in multilinearCurryLeftEquiv R M M₂.

The direct and inverse maps are given by f.curryLeft and f.uncurryLeft. Use these unless you need the full framework of linear equivs.

Equations

• multilinearCurryLeftEquiv R M M₂ = { toFun := MultilinearMap.curryLeft, map_add' := ⋯, map_smul' := ⋯, invFun := LinearMap.uncurryLeft, left_inv := ⋯, right_inv := ⋯ }

Right currying

def MultilinearMap.uncurryRight {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) : MultilinearMap R M M₂

Given a multilinear map f in n variables to the space of linear maps from M (last n) to M₂, construct the corresponding multilinear map on n+1 variables obtained by concatenating the variables, given by m ↦ f (init m) (m (last n))

Equations

• f.uncurryRight = { toFun := fun (m : (i : Fin n.succ) → M i) => (f (Fin.init m)) (m (Fin.last n)), map_update_add' := ⋯, map_update_smul' := ⋯ }

@[simp]

theorem MultilinearMap.uncurryRight_apply {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) (m : (i : Fin n.succ) → M i) : f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))

def MultilinearMap.curryRight {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)

Given a multilinear map f in n+1 variables, split the last variable to obtain a multilinear map in n variables taking values in linear maps from M (last n) to M₂, given by m ↦ (x ↦ f (snoc m x)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MultilinearMap.curryRight_apply {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) (m : (i : Fin n) → M i.castSucc) (x : M (Fin.last n)) : (f.curryRight m) x = f (Fin.snoc m x)

@[simp]

theorem MultilinearMap.curry_uncurryRight {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)) : f.uncurryRight.curryRight = f

@[simp]

theorem MultilinearMap.uncurry_curryRight {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] (f : MultilinearMap R M M₂) : f.curryRight.uncurryRight = f

def multilinearCurryRightEquiv (R : Type uR) {n : ℕ} (M : Fin n.succ → Type v) (M₂ : Type v₂) [CommSemiring R] [(i : Fin n.succ) → AddCommMonoid (M i)] [AddCommMonoid M₂] [(i : Fin n.succ) → Module R (M i)] [Module R M₂] : MultilinearMap R M M₂ ≃ₗ[R] MultilinearMap R (fun (i : Fin n) => M i.castSucc) (M (Fin.last n) →ₗ[R] M₂)

The space of multilinear maps on Π (i : Fin (n+1)), M i is canonically isomorphic to the space of linear maps from the space of multilinear maps on Π (i : Fin n), M (castSucc i) to the space of linear maps on M (last n), by separating the last variable. We register this isomorphism as a linear isomorphism in multilinearCurryRightEquiv R M M₂.

The direct and inverse maps are given by f.curryRight and f.uncurryRight. Use these unless you need the full framework of linear equivs.

Equations

• multilinearCurryRightEquiv R M M₂ = { toFun := MultilinearMap.curryRight, map_add' := ⋯, map_smul' := ⋯, invFun := MultilinearMap.uncurryRight, left_inv := ⋯, right_inv := ⋯ }

def MultilinearMap.currySum {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι ⊕ ι') => M') M₂) : MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)

A multilinear map on ∀ i : ι ⊕ ι', M' defines a multilinear map on ∀ i : ι, M' taking values in the space of multilinear maps on ∀ i : ι', M'.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MultilinearMap.currySum_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι ⊕ ι') => M') M₂) (u : ι → M') (v : ι' → M') : (f.currySum u) v = f (Sum.elim u v)

def MultilinearMap.uncurrySum {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)) : MultilinearMap R (fun (x : ι ⊕ ι') => M') M₂

A multilinear map on ∀ i : ι, M' taking values in the space of multilinear maps on ∀ i : ι', M' defines a multilinear map on ∀ i : ι ⊕ ι', M'.

Equations

• f.uncurrySum = { toFun := fun (u : ι ⊕ ι' → M') => (f (u ∘ Sum.inl)) (u ∘ Sum.inr), map_update_add' := ⋯, map_update_smul' := ⋯ }

@[simp]

theorem MultilinearMap.uncurrySum_aux_apply {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} (f : MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)) (u : ι ⊕ ι' → M') : f.uncurrySum u = (f (u ∘ Sum.inl)) (u ∘ Sum.inr)

def MultilinearMap.currySumEquiv (R : Type uR) (ι : Type uι) (M₂ : Type v₂) (M' : Type v') [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] (ι' : Type u_1) : MultilinearMap R (fun (x : ι ⊕ ι') => M') M₂ ≃ₗ[R] MultilinearMap R (fun (x : ι) => M') (MultilinearMap R (fun (x : ι') => M') M₂)

Linear equivalence between the space of multilinear maps on ∀ i : ι ⊕ ι', M' and the space of multilinear maps on ∀ i : ι, M' taking values in the space of multilinear maps on ∀ i : ι', M'.

Equations

• MultilinearMap.currySumEquiv R ι M₂ M' ι' = { toFun := MultilinearMap.currySum, map_add' := ⋯, map_smul' := ⋯, invFun := MultilinearMap.uncurrySum, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MultilinearMap.coe_currySumEquiv {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} : ⇑(currySumEquiv R ι M₂ M' ι') = currySum

@[simp]

theorem MultilinearMap.coe_currySumEquiv_symm {R : Type uR} {ι : Type uι} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {ι' : Type u_1} : ⇑(currySumEquiv R ι M₂ M' ι').symm = uncurrySum

def MultilinearMap.curryFinFinset (R : Type uR) (M₂ : Type v₂) (M' : Type v') [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) : MultilinearMap R (fun (x : Fin n) => M') M₂ ≃ₗ[R] MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)

If s : Finset (Fin n) is a finite set of cardinality k and its complement has cardinality l, then the space of multilinear maps on fun i : Fin n => M' is isomorphic to the space of multilinear maps on fun i : Fin k => M' taking values in the space of multilinear maps on fun i : Fin l => M'.

Equations

• MultilinearMap.curryFinFinset R M₂ M' hk hl = (MultilinearMap.domDomCongrLinearEquiv R R M' M₂ (finSumEquivOfFinset hk hl).symm).trans (MultilinearMap.currySumEquiv R (Fin k) M₂ M' (Fin l))

@[simp]

theorem MultilinearMap.curryFinFinset_apply {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun (x : Fin n) => M') M₂) (mk : Fin k → M') (ml : Fin l → M') : (((curryFinFinset R M₂ M' hk hl) f) mk) ml = f fun (i : Fin n) => Sum.elim mk ml ((finSumEquivOfFinset hk hl).symm i)

@[simp]

theorem MultilinearMap.curryFinFinset_symm_apply {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (m : Fin n → M') : ((curryFinFinset R M₂ M' hk hl).symm f) m = (f fun (i : Fin k) => m ((finSumEquivOfFinset hk hl) (Sum.inl i))) fun (i : Fin l) => m ((finSumEquivOfFinset hk hl) (Sum.inr i))

theorem MultilinearMap.curryFinFinset_symm_apply_piecewise_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (x y : M') : ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y) = (f fun (x_1 : Fin k) => x) fun (x : Fin l) => y

@[simp]

theorem MultilinearMap.curryFinFinset_symm_apply_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun (x : Fin k) => M') (MultilinearMap R (fun (x : Fin l) => M') M₂)) (x : M') : (((curryFinFinset R M₂ M' hk hl).symm f) fun (x_1 : Fin n) => x) = (f fun (x_1 : Fin k) => x) fun (x_1 : Fin l) => x

theorem MultilinearMap.curryFinFinset_apply_const {R : Type uR} {M₂ : Type v₂} {M' : Type v'} [CommSemiring R] [AddCommMonoid M'] [AddCommMonoid M₂] [Module R M'] [Module R M₂] {k l n : ℕ} {s : Finset (Fin n)} (hk : s.card = k) (hl : sᶜ.card = l) (f : MultilinearMap R (fun (x : Fin n) => M') M₂) (x y : M') : ((((curryFinFinset R M₂ M' hk hl) f) fun (x_1 : Fin k) => x) fun (x : Fin l) => y) = f (s.piecewise (fun (x_1 : Fin n) => x) fun (x : Fin n) => y)