Witt's extension theorem for symplectic vector spaces

Let (V, ω₁) and (W, ω₂) be finite-dimensional real symplectic vector spaces of the same dimension, S a subspace of V and f : S → W an injective linear map preserving the restricted forms, ω₂ (f x) (f y) = ω₁ x y. Witt's extension theorem says that f is the restriction of a linear symplectomorphism e : V ≃ₗ[ℝ] W (TauCeti.SymplecticForm.exists_isSymplectomorphism_extend). The subspace S is arbitrary: it may be isotropic, symplectic, or degenerate of any rank. The case S = 0 is the linear Darboux theorem, that any two symplectic vector spaces of the same dimension are symplectomorphic (TauCeti.SymplecticForm.exists_isSymplectomorphism).

The proof extends f one vector at a time, as a partial linear map V →ₗ.[ℝ] W, until its domain is all of V. Write T for the image of f. Given v ∉ S, a vector v' ∉ T with ω₂ (f s) v' = ω₁ s v for all s ∈ S lets f extend to S ⊕ ℝ v by v ↦ v', injectively and isometrically. Such a pair exists for a suitable v:

• if S is coisotropic, S^ω ≤ S, any v ∉ S works: nondegeneracy of ω₂ gives a v' with the prescribed pairings, and v' = f s₀ would put v - s₀ in S^ω ≤ S;
• otherwise pick v ∈ S^ω outside S, and v' ∈ T^ω outside T. Such a v' exists because T is not coisotropic either: f carries the radical S ∩ S^ω onto the radical T ∩ T^ω, and S^ω, T^ω have the same dimension, so S^ω ≤ S exactly when T^ω ≤ T.

Main results

• TauCeti.SymplecticForm.exists_isSymplectomorphism_extend: an injective linear map from a subspace preserving the forms extends to a symplectomorphism.
• TauCeti.SymplecticForm.exists_isSymplectomorphism_extend_linearEquiv: the same for a linear isomorphism between two subspaces.
• TauCeti.SymplecticForm.exists_isSymplectomorphism: two symplectic vector spaces of the same finite dimension are symplectomorphic.

References

• D. McDuff and D. Salamon, Introduction to Symplectic Topology, 3rd ed., Oxford, 2017, Section 2.1 (linear symplectic geometry).
• E. Artin, Geometric Algebra, Interscience, 1957, Chapter III, Theorem 3.9 (Witt's theorem).

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism_extend {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ V] [FiniteDimensional ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (hdim : Module.finrank ℝ V = Module.finrank ℝ W) {S : Submodule ℝ V} (f : ↥S →ₗ[ℝ] W) (hf : Function.Injective ⇑f) (hω : ∀ (x y : ↥S), (fun (v w : W) => (ω₂.toBilinForm v) w) (f x) (f y) = (fun (v w : V) => (ω₁.toBilinForm v) w) ↑x ↑y) : ∃ (e : V ≃ₗ[ℝ] W), ω₁.IsSymplectomorphism ω₂ e ∧ ∀ (x : ↥S), e ↑x = f x

Witt's extension theorem for symplectic vector spaces. Between two finite-dimensional symplectic vector spaces of the same dimension, an injective linear map from an arbitrary subspace S preserving the restricted forms extends to a linear symplectomorphism. The subspace S need not be symplectic: the restricted form may be degenerate of any rank.

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism_extend_linearEquiv {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ V] [FiniteDimensional ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (hdim : Module.finrank ℝ V = Module.finrank ℝ W) {S : Submodule ℝ V} {T : Submodule ℝ W} (f : ↥S ≃ₗ[ℝ] ↥T) (hω : ∀ (x y : ↥S), (fun (v w : W) => (ω₂.toBilinForm v) w) ↑(f x) ↑(f y) = (fun (v w : V) => (ω₁.toBilinForm v) w) ↑x ↑y) : ∃ (e : V ≃ₗ[ℝ] W), ω₁.IsSymplectomorphism ω₂ e ∧ ∀ (x : ↥S), e ↑x = ↑(f x)

Witt's extension theorem, for a linear isomorphism f : S ≃ₗ[ℝ] T between subspaces of two symplectic vector spaces of the same finite dimension: if f preserves the restricted forms, it is the restriction of a linear symplectomorphism.

theorem TauCeti.SymplecticForm.exists_isSymplectomorphism {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W] [FiniteDimensional ℝ V] [FiniteDimensional ℝ W] (ω₁ : SymplecticForm V) (ω₂ : SymplecticForm W) (hdim : Module.finrank ℝ V = Module.finrank ℝ W) : ∃ (e : V ≃ₗ[ℝ] W), ω₁.IsSymplectomorphism ω₂ e

Linear Darboux theorem. Two symplectic vector spaces of the same finite dimension are linearly symplectomorphic.