Symplectic bases of alternating bilinear forms

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). BACKLOG #50, the linear-algebra half of the standard form of Darboux's theorem.

Every non-degenerate alternating bilinear form on a finite-dimensional vector space, over any field, has a symplectic basis p₁, …, pₙ, q₁, …, qₙ: B pᵢ pⱼ = 0, B qᵢ qⱼ = 0, B pᵢ qⱼ = δᵢⱼ. So the dimension is even, and in the coordinates of the basis the form is the standard one, B u v = ∑ᵢ (u_{pᵢ} v_{qᵢ} − u_{qᵢ} v_{pᵢ}).

• LinearMap.BilinForm.IsSymplecticBasis — the predicate on a basis indexed by ι ⊕ ι (inl = the p's, inr = the q's); IsSymplecticBasis.reindex, .inl_inr, .inr_inl;
• ★★ LinearMap.BilinForm.IsAlt.exists_isSymplecticBasis — existence, by induction on the dimension (Gram–Schmidt for alternating forms): pick p ≠ 0 and q with B p q = 1, split off the symplectic plane span {p, q} against its B-orthogonal complement (isCompl_orthogonal_of_restrict_nondegenerate), on which the form stays non-degenerate, and recurse; the basis is indexed by Fin n ⊕ Fin n;
• ★ LinearMap.BilinForm.IsAlt.even_finrank — the dimension is even;
• ★ LinearMap.BilinForm.IsSymplecticBasis.apply_eq_sum — the standard form in symplectic coordinates.

Mathlib at the pin has orthogonal bases for symmetric forms only (LinearMap.BilinForm.iIsOrtho) and the symplectic group of matrices (Matrix.J), not the normal form of an alternating form. The consumer is Geometry/Manifold/DarbouxStandardForm.lean (the ∑ dpᵢ ∧ dqᵢ form of Darboux's theorem); specs/BACKLOG.md #50; specs/generator-layer-scoping.md Q31.

structure LinearMap.BilinForm.IsSymplecticBasis {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (B : LinearMap.BilinForm K V) {ι : Type u_3} (e : Module.Basis (ι ⊕ ι) K V) : Prop

A basis e indexed by ι ⊕ ι is symplectic for B when the inl-vectors (the p's) are pairwise B-orthogonal, so are the inr-vectors (the q's), and B pᵢ qⱼ = δᵢⱼ.

• inl_inl (i j : ι) : (B (e (Sum.inl i))) (e (Sum.inl j)) = 0
• inr_inr (i j : ι) : (B (e (Sum.inr i))) (e (Sum.inr j)) = 0
• inl_inr_self (i : ι) : (B (e (Sum.inl i))) (e (Sum.inr i)) = 1
• inl_inr_of_ne (i j : ι) : i ≠ j → (B (e (Sum.inl i))) (e (Sum.inr j)) = 0

theorem LinearMap.BilinForm.IsSymplecticBasis.inl_inr {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {ι : Type u_3} {e : Module.Basis (ι ⊕ ι) K V} [DecidableEq ι] (h : B.IsSymplecticBasis e) (i j : ι) : (B (e (Sum.inl i))) (e (Sum.inr j)) = if i = j then 1 else 0

theorem LinearMap.BilinForm.IsSymplecticBasis.inr_inl {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {ι : Type u_3} {e : Module.Basis (ι ⊕ ι) K V} [DecidableEq ι] (hB : B.IsAlt) (h : B.IsSymplecticBasis e) (i j : ι) : (B (e (Sum.inr i))) (e (Sum.inl j)) = if j = i then -1 else 0

theorem LinearMap.BilinForm.IsSymplecticBasis.reindex {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {ι : Type u_3} {e : Module.Basis (ι ⊕ ι) K V} (h : B.IsSymplecticBasis e) {ι' : Type u_4} (σ : ι ≃ ι') : B.IsSymplecticBasis (e.reindex (σ.sumCongr σ))

A symplectic basis stays symplectic under a re-indexing applied to both halves.

theorem LinearMap.BilinForm.IsSymplecticBasis.apply_eq_sum {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {B : LinearMap.BilinForm K V} {ι : Type u_3} {e : Module.Basis (ι ⊕ ι) K V} [Fintype ι] [DecidableEq ι] (hB : B.IsAlt) (h : B.IsSymplecticBasis e) (u v : V) : (B u) v = ∑ i : ι, ((e.repr u) (Sum.inl i) * (e.repr v) (Sum.inr i) - (e.repr u) (Sum.inr i) * (e.repr v) (Sum.inl i))

★ The standard form in symplectic coordinates: B u v = ∑ᵢ (u_{pᵢ} v_{qᵢ} − u_{qᵢ} v_{pᵢ}).

def LinearMap.BilinForm.planeSumEquiv (ι : Type u_3) : Fin 2 ⊕ ι ⊕ ι ≃ Option ι ⊕ Option ι

The index re-shuffle joining a symplectic plane (indexed by Fin 2: 0 the p, 1 the q) to a symplectic basis indexed by ι ⊕ ι, giving one indexed by Option ι ⊕ Option ι with the plane at none.

Equations

• One or more equations did not get rendered due to their size.

theorem LinearMap.BilinForm.IsAlt.exists_isSymplecticBasis_aux {K : Type u} [Field K] (n : ℕ) (V : Type v) [AddCommGroup V] [Module K V] [FiniteDimensional K V] (B : LinearMap.BilinForm K V) : B.IsAlt → B.Nondegenerate → Module.finrank K V = n → ∃ (ι : Type v) (x : Fintype ι) (e : Module.Basis (ι ⊕ ι) K V), B.IsSymplecticBasis e

The induction behind exists_isSymplecticBasis, on the dimension, generalised over the space: a non-degenerate alternating form on a space of dimension n has a symplectic basis indexed by some finite ι ⊕ ι.

theorem LinearMap.BilinForm.IsAlt.exists_isSymplecticBasis {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.IsAlt) (hnd : B.Nondegenerate) : ∃ (n : ℕ) (e : Module.Basis (Fin n ⊕ Fin n) K V), B.IsSymplecticBasis e

★★ Every non-degenerate alternating form has a symplectic basis (Gram–Schmidt for alternating forms): a basis p₁, …, pₙ, q₁, …, qₙ with B pᵢ pⱼ = 0, B qᵢ qⱼ = 0, B pᵢ qⱼ = δᵢⱼ.

theorem LinearMap.BilinForm.IsAlt.even_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {B : LinearMap.BilinForm K V} (hB : B.IsAlt) (hnd : B.Nondegenerate) : Even (Module.finrank K V)

★ A space carrying a non-degenerate alternating form has even dimension.