structure SymplecticLinearAlgebra.IsSymplecticForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) : Prop

A bilinear form $\Omega$ on a real vector space $V$ is symplectic iff it is alternating ($\Omega(v,v) = 0$) and nondegenerate (its left radical is trivial).

• alt : Ω.IsAlt
• nondeg : LinearMap.SeparatingLeft Ω

def SymplecticLinearAlgebra.symplecticOrtho {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (E : Submodule ℝ V) : Submodule ℝ V

The symplectic orthogonal $E^\Omega = \{v \in V : \Omega(v, e) = 0 \text{ for all } e \in E\}$.

def SymplecticLinearAlgebra.IsSymplecticSubspace {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (E : Submodule ℝ V) : Prop

A subspace $E$ is symplectic with respect to $\Omega$ iff $E \cap E^\Omega = \{0\}$ (Definition 4 in the textbook).

def SymplecticLinearAlgebra.IsLagrangian {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (E : Submodule ℝ V) : Prop

A subspace $E$ is Lagrangian iff $E^\Omega = E$, equivalently isotropic and half-dimensional (Definition 5 in the textbook).

theorem SymplecticLinearAlgebra.sympl_skew {V : Type u_1} [AddCommGroup V] [Module ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hAlt : Ω.IsAlt) (x y : V) : (Ω x) y = -(Ω y) x

An alternating bilinear form is skew-symmetric: $\Omega(x, y) = -\Omega(y, x)$.

theorem SymplecticLinearAlgebra.IsSymplecticForm.orthogonal_top_eq_bot {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) : Ω.orthogonal ⊤ = ⊥

For a symplectic form on a finite-dimensional space, the orthogonal of the whole space is trivial: $V^\Omega = \{0\}$ (equivalent to nondegeneracy).

theorem SymplecticLinearAlgebra.symplecticOrtho_finrank_add {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) (E : Submodule ℝ V) : Module.finrank ℝ ↥E + Module.finrank ℝ ↥(symplecticOrtho Ω E) = Module.finrank ℝ V

Dimension formula for the symplectic orthogonal: $\dim E + \dim E^\Omega = \dim V$.

theorem SymplecticLinearAlgebra.symplectic_subspace_iff {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) (E : Submodule ℝ V) : IsSymplecticSubspace Ω E ↔ IsCompl E (symplecticOrtho Ω E)

$E$ is a symplectic subspace iff $E$ and $E^\Omega$ are complementary: $V = E \oplus E^\Omega$.

theorem SymplecticLinearAlgebra.lagrangian_half_dim {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) {E : Submodule ℝ V} (hE : IsLagrangian Ω E) : 2 * Module.finrank ℝ ↥E = Module.finrank ℝ V

A Lagrangian subspace has half the dimension of the ambient symplectic space: $2 \dim E = \dim V$.

noncomputable def SymplecticLinearAlgebra.symplRestrict {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (E : Submodule ℝ V) : V →ₗ[ℝ] ↥E →ₗ[ℝ] ℝ

The linear map $V \to E^*$ sending $v \mapsto \Omega(\cdot, v)|_E$, used to identify $V/E$ with the dual of a Lagrangian.

theorem SymplecticLinearAlgebra.ker_symplRestrict {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (E : Submodule ℝ V) : (symplRestrict Ω E).ker = Ω.orthogonal E

The kernel of symplRestrict Ω E is exactly the symplectic orthogonal $E^\Omega$.

noncomputable def SymplecticLinearAlgebra.lagrangianQuotientDualEquiv {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {Ω : LinearMap.BilinForm ℝ V} (hΩ : IsSymplecticForm Ω) {E : Submodule ℝ V} (hE : IsLagrangian Ω E) : (V ⧸ E) ≃ₗ[ℝ] ↥E →ₗ[ℝ] ℝ

For a Lagrangian subspace $E$, the symplectic form induces a canonical isomorphism $V/E \simeq E^*$.

noncomputable def SymplecticLinearAlgebra.wedgePowBilinFormAux {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (hAlt : Ω.IsAlt) (n : ℕ) : V [⋀^Fin (2 * n)]→ₗ[ℝ] ℝ

Recursive construction of the $n$-fold wedge power $\Omega^{\wedge n}$ as an alternating $2n$-form, built by inductively wedging with the $2$-form $\Omega$.

noncomputable def SymplecticLinearAlgebra.wedgePowBilinForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] (Ω : LinearMap.BilinForm ℝ V) (hAlt : Ω.IsAlt) (m : ℕ) : V [⋀^Fin m]→ₗ[ℝ] ℝ

Wedge power $\Omega^{\wedge n}$ packaged as an alternating $m$-form: equals wedgePowBilinFormAux when $m = 2n$ is even, and zero otherwise.

noncomputable def SymplecticLinearAlgebra.symplecticVolumeForm {V : Type u_1} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (Ω : LinearMap.BilinForm ℝ V) (hΩ : IsSymplecticForm Ω) : V [⋀^Fin (Module.finrank ℝ V)]→ₗ[ℝ] ℝ

The symplectic volume form $\frac{1}{n!}\Omega^{\wedge n}$ where $\dim V = 2n$ (Definition 6 in the textbook).