structure SymplecticLinearAlgebra.SymplecticBasis {V : Type u_2} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) : Type u_2

A standard symplectic basis $\{e_i, f_i\}_{i=1}^n$ for $(V, \Omega)$: the $e_i, f_i$ form a basis of $V$ and satisfy $\Omega(e_i, e_j) = \Omega(f_i, f_j) = 0$ and $\Omega(e_i, f_j) = \delta_{ij}$.

• n : ℕ
• e : Fin self.n → V
• f : Fin self.n → V
• basis : Module.Basis (Fin self.n ⊕ Fin self.n) ℝ V
• basis_eq_e (i : Fin self.n) : self.basis (Sum.inl i) = self.e i
• basis_eq_f (i : Fin self.n) : self.basis (Sum.inr i) = self.f i
• omega_ee (i j : Fin self.n) : (Ω (self.e i)) (self.e j) = 0
• omega_ff (i j : Fin self.n) : (Ω (self.f i)) (self.f j) = 0
• omega_ef (i j : Fin self.n) : (Ω (self.e i)) (self.f j) = if i = j then 1 else 0

theorem SymplecticLinearAlgebra.exists_symplectic_pair {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) (hne : Nontrivial V) : ∃ (e₁ : V) (f₁ : V), (Ω e₁) f₁ = 1 ∧ IsSymplecticSubspace Ω (Submodule.span ℝ {e₁, f₁})

Existence of a symplectic pair: on a nontrivial finite-dimensional symplectic space, there exist $e_1, f_1$ with $\Omega(e_1, f_1) = 1$ spanning a 2-dimensional symplectic subspace.

theorem SymplecticLinearAlgebra.restrict_symplecticOrtho_symplectic {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) {P : Submodule ℝ V} (hCompl : IsCompl P (symplecticOrtho Ω P)) : IsSymplecticForm (Ω.restrict (symplecticOrtho Ω P))

If $P$ and its symplectic orthogonal $P^\Omega$ form a complementary decomposition of $V$, then $\Omega$ restricted to $P^\Omega$ is itself symplectic.

theorem SymplecticLinearAlgebra.ortho_of_mem_symplecticOrtho {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) {P : Submodule ℝ V} {u : V} (hu : u ∈ symplecticOrtho Ω P) {p : V} (hp : p ∈ P) : (Ω u) p = 0

An element of the symplectic orthogonal $P^\Omega$ pairs trivially with every $p \in P$: $\Omega(u, p) = 0$.

theorem SymplecticLinearAlgebra.symplectic_standard_basis {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) : ∃ (n : ℕ) (e : Fin n → V) (f : Fin n → V), Module.finrank ℝ V = 2 * n ∧ (∀ (i j : Fin n), (Ω (e i)) (e j) = 0) ∧ (∀ (i j : Fin n), (Ω (f i)) (f j) = 0) ∧ (∀ (i j : Fin n), (Ω (e i)) (f j) = if i = j then 1 else 0) ∧ LinearIndependent ℝ (Sum.elim e f) ∧ ⊤ ≤ Submodule.span ℝ (Set.range (Sum.elim e f))

Standard symplectic basis theorem: every finite-dimensional symplectic space $(V, \Omega)$ has even dimension $2n$ and admits a basis $\{e_i, f_i\}_{i=1}^n$ with $\Omega(e_i, e_j) = \Omega(f_i, f_j) = 0$ and $\Omega(e_i, f_j) = \delta_{ij}$.