Alternatization of a continuous bilinear map

A continuous bilinear map B : E →L[𝕜] E →L[𝕜] F has the alternatization (v₀, v₁) ↦ B v₀ v₁ - B v₁ v₀, a continuous alternating map in two arguments. This file packages that operation as the continuous linear map ContinuousAlternatingMap.alternatizeBilinCLM 𝕜 E F from bilinear maps to alternating two-forms: E →L[𝕜] F is identified with the continuous alternating maps in one argument and Mathlib's ContinuousAlternatingMap.alternatizeUncurryFinCLM is applied. Being a continuous linear map, the operator transports smoothness, so a smooth family of bilinear maps has a smooth alternatization. As in Mathlib's alternatizeUncurryFin, no factor 2⁻¹ is built in, so the construction is available over every normed field.

Main declarations

• TauCeti.ContinuousAlternatingMap.alternatizeBilinCLM: the alternatization of continuous bilinear maps, as a continuous linear map into the continuous alternating two-forms.
• TauCeti.ContinuousAlternatingMap.alternatizeBilinCLM_apply: it evaluates to B (v 0) (v 1) - B (v 1) (v 0).

noncomputable def TauCeti.ContinuousAlternatingMap.alternatizeBilinCLM (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : (E →L[𝕜] E →L[𝕜] F) →L[𝕜] E [⋀^Fin 2]→L[𝕜] F

The alternatization B ↦ ((v₀, v₁) ↦ B v₀ v₁ - B v₁ v₀) of a continuous bilinear map, as a continuous linear map into the continuous alternating two-forms. It is Mathlib's ContinuousAlternatingMap.alternatizeUncurryFinCLM in one alternating argument, precomposed with the identification of E →L[𝕜] F with the continuous alternating maps in one argument.

Equations

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

@[simp]

theorem TauCeti.ContinuousAlternatingMap.alternatizeBilinCLM_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (B : E →L[𝕜] E →L[𝕜] F) (v : Fin 2 → E) : ((alternatizeBilinCLM 𝕜 E F) B) v = (B (v 0)) (v 1) - (B (v 1)) (v 0)

The alternatization of a continuous bilinear map B evaluates on v : Fin 2 → E to B (v 0) (v 1) - B (v 1) (v 0).