Currying continuous alternating forms

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

noncomputable def ContinuousAlternatingMap.curryLeft {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : E →L[𝕜] E [⋀^Fin n]→L[𝕜] F

Given a continuous alternating map f in n+1 variables, split the first variable to obtain a continuous linear map into continuous 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 ContinuousMultilinearMap.curryLeft for AlternatingMap. See also ContinuousAlternatingMap.curryLeftLI.

Equations

• f.curryLeft = AlternatingMap.mkContinuousLinear f.toAlternatingMap.curryLeft ‖f‖ ⋯

@[simp]

theorem ContinuousAlternatingMap.toContinuousMultilinearMap_curryLeft {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) : (f.curryLeft x).toContinuousMultilinearMap = f.curryLeft x

@[simp]

theorem ContinuousAlternatingMap.toAlternatingMap_curryLeft {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) : (f.curryLeft x).toAlternatingMap = f.toAlternatingMap.curryLeft x

@[simp]

theorem ContinuousAlternatingMap.norm_curryLeft {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : ‖f.curryLeft‖ = ‖f‖

@[simp]

theorem ContinuousAlternatingMap.curryLeft_apply_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) (v : Fin n → E) : (f.curryLeft x) v = f (Matrix.vecCons x v)

@[simp]

theorem ContinuousAlternatingMap.curryLeft_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} : curryLeft 0 = 0

@[simp]

theorem ContinuousAlternatingMap.curryLeft_add {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f g : E [⋀^Fin (n + 1)]→L[𝕜] F) : (f + g).curryLeft = f.curryLeft + g.curryLeft

@[simp]

theorem ContinuousAlternatingMap.curryLeft_smul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (r : 𝕜) (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : (r • f).curryLeft = r • f.curryLeft

noncomputable def ContinuousAlternatingMap.curryLeftLI {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} : E [⋀^Fin (n + 1)]→L[𝕜] F →ₗᵢ[𝕜] E →L[𝕜] E [⋀^Fin n]→L[𝕜] F

ContinuousAlternatingMap.curryLeft as a LinearIsometry.

Equations

• ContinuousAlternatingMap.curryLeftLI = { toFun := fun (f : E [⋀^Fin (n + 1)]→L[𝕜] F) => f.curryLeft, map_add' := ⋯, map_smul' := ⋯, norm_map' := ⋯ }

@[simp]

theorem ContinuousAlternatingMap.curryLeftLI_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[𝕜] F) : curryLeftLI f = f.curryLeft

@[simp]

theorem ContinuousAlternatingMap.curryLeft_same {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {n : ℕ} (f : E [⋀^Fin (n + 2)]→L[𝕜] F) (x : E) : (f.curryLeft x).curryLeft x = 0

Currying with the same element twice gives the zero map.

@[simp]

theorem ContinuousAlternatingMap.curryLeft_compContinuousAlternatingMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (g : F →L[𝕜] G) (f : E [⋀^Fin (n + 1)]→L[𝕜] F) (x : E) : (g.compContinuousAlternatingMap f).curryLeft x = g.compContinuousAlternatingMap (f.curryLeft x)

@[simp]

theorem ContinuousAlternatingMap.curryLeft_compContinuousLinearMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ} (g : F [⋀^Fin (n + 1)]→L[𝕜] G) (f : E →L[𝕜] F) (x : E) : (g.compContinuousLinearMap f).curryLeft x = (g.curryLeft (f x)).compContinuousLinearMap f