Comparing normed and topological interior products

The normed ContinuousAlternatingMap.curryLeft agrees pointwise with the norm-free ContinuousAlternatingMap.curryLeftTopological. This comparison lets normed applications use the topological interior-product API without importing wedge constructions.

Currying a continuous alternating map of two vectors in its first slot and reading the result as a linear map gives its flat map f ↦ (v ↦ f(v, ·)), a continuous linear map ContinuousAlternatingMap.flatL.

theorem ContinuousAlternatingMap.curryLeft_eq_curryLeftTopological {E : Type u_1} {F₁ : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F₁] [NormedSpace ℝ F₁] {n : ℕ} (f : E [⋀^Fin (n + 1)]→L[ℝ] F₁) (x : E) : f.curryLeft x = f.curryLeftTopological x

The normed and norm-free interior products agree on normed spaces.

noncomputable def ContinuousAlternatingMap.flatL (𝕜 : Type u_3) (E : Type u_4) (F : Type u_5) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : E [⋀^Fin 2]→L[𝕜] F →L[𝕜] E →L[𝕜] E →L[𝕜] F

The flat map of continuous alternating maps of two vectors, f ↦ (v ↦ f(v, ·)): currying in the first slot, then reading the resulting alternating map of one vector as a linear map.

@[simp]

theorem ContinuousAlternatingMap.ofSubsingleton_flatL_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E [⋀^Fin 2]→L[𝕜] F) (v : E) : (ofSubsingleton 𝕜 E F 0) (((flatL 𝕜 E F) f) v) = f.curryLeft v

The flat map of f at v, read back as an alternating map of one vector, is the curried map f(v, ·).

@[simp]

theorem ContinuousAlternatingMap.flatL_apply_apply {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E [⋀^Fin 2]→L[𝕜] F) (v w : E) : (((flatL 𝕜 E F) f) v) w = f ![v, w]

The flat map evaluates the alternating map on the pair.