Symplectic structure of alternating nondegenerate bilinear forms

For a finite-dimensional complex vector space V equipped with an alternating nondegenerate bilinear form B:

• Symplectic splitting (exists_symplectic_splitting): there exist v, w with B v w = 1, B w v = −1, spanning a 2-dimensional nondegenerate plane U whose orthogonal complement U^⊥ inherits an alternating nondegenerate restriction of B with finrank ℂ U^⊥ = finrank ℂ V − 2.

• Standard basis (exists_symplectic_basis): iterating the splitting gives a basis indexed by Fin (2 * ℓ) in two blocks — the first ℓ vectors and their partners — carrying the canonical symplectic pairing matrix. In particular the dimension of V is even.

The assembly interleaves the plane's basis with the complement's through Basis.prod, Submodule.prodEquivOfIsCompl and the reindexing symplecticReindexEquiv on Fin (2 * ℓ).

The symplectic plane

Disjointness of the symplectic plane and its orthogonal complement

Symplectic splitting

theorem RS.exists_symplectic_splitting {V : Type u_1} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] {B : LinearMap.BilinForm ℂ V} (hAlt : B.IsAlt) (hND : B.Nondegenerate) (hPos : 0 < Module.finrank ℂ V) : ∃ (v : V) (w : V), (B v) w = 1 ∧ (B w) v = -1 ∧ have U := Submodule.span ℂ {v, w}; (B.restrict U).Nondegenerate ∧ IsCompl U (B.orthogonal U) ∧ (B.restrict (B.orthogonal U)).IsAlt ∧ (B.restrict (B.orthogonal U)).Nondegenerate ∧ Module.finrank ℂ ↥(B.orthogonal U) = Module.finrank ℂ V - 2

Symplectic splitting: given V with an alternating nondegenerate bilinear form B and finrank ℂ V ≥ 1, there exist vectors v, w spanning a 2-dimensional symplectic plane U such that B v w = 1, B w v = −1, and the orthogonal complement U^⊥ carries an alternating nondegenerate restriction of B with finrank ℂ U^⊥ = finrank ℂ V − 2.

Symplectic basis assembly

theorem RS.exists_symplectic_basis {V : Type} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (B : LinearMap.BilinForm ℂ V) (hAlt : B.IsAlt) (hND : B.Nondegenerate) : ∃ (ℓ : ℕ) (_ : Module.finrank ℂ V = 2 * ℓ) (f : Module.Basis (Fin (2 * ℓ)) ℂ V), ∀ (i j : Fin (2 * ℓ)), (B (f i)) (f j) = if ↑i + ℓ = ↑j then 1 else if ↑j + ℓ = ↑i then -1 else 0

Symplectic standard basis: a finite-dimensional complex vector space carrying an alternating nondegenerate bilinear form admits a basis indexed by Fin (2 * ℓ) in two blocks — the first ℓ vectors and their partners — with the canonical symplectic pairing matrix: B(eₘ, eₘ₊ℓ) = 1, B(eₘ₊ℓ, eₘ) = −1, and all other pairings vanish.