Symplectic forms from continuous alternating two-forms

SymplecticForm.ofContinuousAlternatingMap reads a nondegenerate continuous alternating map in two variables as an algebraic symplectic form. Nondegeneracy need only be checked in the left variable, since alternation supplies the corresponding right-variable condition. The evaluation lemma identifies the resulting bilinear form with the original two-form. Over finite-dimensional spaces, Witt's extension theorem then gives a continuous linear automorphism of E × N fixing E × {0} and carrying one nondegenerate two-form to another with the same restriction to E × {0}.

def TauCeti.SymplecticForm.ofContinuousAlternatingMap {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] (ω : V [⋀^Fin 2]→L[ℝ] ℝ) (hnd : ∀ (v : V), (∀ (w : V), ω ![v, w] = 0) → v = 0) : SymplecticForm V

A continuous alternating two-form with trivial left kernel gives an algebraic symplectic form. No finite-dimensionality assumption is needed.

@[simp]

theorem TauCeti.SymplecticForm.ofContinuousAlternatingMap_apply {V : Type u_1} [AddCommGroup V] [Module ℝ V] [TopologicalSpace V] (ω : V [⋀^Fin 2]→L[ℝ] ℝ) (hnd : ∀ (v : V), (∀ (w : V), ω ![v, w] = 0) → v = 0) (v w : V) : (fun (v w : V) => ((ofContinuousAlternatingMap ω hnd).toBilinForm v) w) v w = ω ![v, w]

The symplectic form constructed from a continuous two-form has the same evaluations.

theorem TauCeti.exists_continuousLinearEquiv_fix_inl_of_compContinuousLinearMap_inl_eq {E : Type u_1} {N : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup N] [NormedSpace ℝ N] [FiniteDimensional ℝ N] {a₀ a₁ : (E × N) [⋀^Fin 2]→L[ℝ] ℝ} (hnd₀ : ∀ (v : E × N), (∀ (w : E × N), a₀ ![v, w] = 0) → v = 0) (hnd₁ : ∀ (v : E × N), (∀ (w : E × N), a₁ ![v, w] = 0) → v = 0) (htan : a₁.compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N) = a₀.compContinuousLinearMap (ContinuousLinearMap.inl ℝ E N)) : ∃ (A : (E × N) ≃L[ℝ] E × N), (∀ (v w : E × N), a₁ ![A v, A w] = a₀ ![v, w]) ∧ ∀ (q : E), A (q, 0) = (q, 0)

Witt's extension theorem for the zero section. If two alternating forms a₀, a₁ on E × N are nondegenerate and have the same restriction to E × {0}, then some continuous linear automorphism A of E × N fixes E × {0} pointwise and carries a₀ to a₁.