Symplectic bases extending a prescribed Lagrangian basis

Every basis of a Lagrangian subspace of a finite-dimensional symplectic space extends to a symplectic basis, with the original vectors at the Sum.inl positions. In particular, an ordered basis adapted to a flag in the Lagrangian retains that flag after the extension. This allows a triangularizing basis on an invariant Lagrangian to be used as the isotropic half of symplectic coordinates.

The construction works in every characteristic. First extend the coordinate functionals of the prescribed basis to the ambient space using Mathlib's Subspace.dualLift, then use LinearMap.BilinForm.toDual to find dual partners. Correct the partners by a strictly triangular combination of the original vectors to make them isotropic. The correction uses no division by two and is proved over a commutative ring.

The resulting family is a basis by the Gram determinant criterion LinearMap.BilinForm.linearIndependent_of_det_ne_zero and dimension counting.

Our convention is Mathlib's Matrix.J: the dual vector pairs to 1 with its prescribed partner, and the prescribed vector pairs to -1 with its dual.

References

• E. Artin, Geometric Algebra (1957), Theorem 3.7.
• J. S. Milne, Algebraic Groups (2017), §24.6 (symplectic groups and isotropic flags).

theorem LinearMap.BilinForm.IsAlt.exists_dual_isotropic_family {R : Type u_1} {V : Type u_2} [CommRing R] [AddCommGroup V] [Module R V] {ι : Type u_3} [Finite ι] [DecidableEq ι] {B : LinearMap.BilinForm R V} (hB : B.IsAlt) (e f : ι → V) (he : ∀ (i j : ι), (B (e i)) (e j) = 0) (hfe : ∀ (i j : ι), (B (f i)) (e j) = if i = j then 1 else 0) : ∃ (f' : ι → V), (∀ (i j : ι), (B (f' i)) (e j) = if i = j then 1 else 0) ∧ ∀ (i j : ι), (B (f' i)) (f' j) = 0

Dual partners of an isotropic family can be chosen isotropic, over any commutative ring. Here B (f i) (e j) = δᵢⱼ fixes the signs to agree with Matrix.J.

theorem LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J_inl_eq_of_finrank {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {B : LinearMap.BilinForm K V} (hB : B.IsAlt) (hnd : B.Nondegenerate) {U : Submodule K V} (e : Module.Basis ι K ↥U) (hU : U ≤ B.orthogonal U) (hdim : Fintype.card ι + Fintype.card ι = Module.finrank K V) : ∃ (b : Module.Basis (ι ⊕ ι) K V), (toMatrix b) B = Matrix.J ι K ∧ ∀ (i : ι), b (Sum.inl i) = ↑(e i)

A prescribed basis of an isotropic subspace of half the ambient dimension extends to a symplectic basis. The original basis vectors occupy the Sum.inl positions, in their given order; the result holds in characteristic two as well.

theorem LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J_inl_eq {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {ι : Type u_3} [Fintype ι] [DecidableEq ι] {B : LinearMap.BilinForm K V} (hB : B.IsAlt) (hnd : B.Nondegenerate) {U : Submodule K V} (e : Module.Basis ι K ↥U) (hU : U = B.orthogonal U) : ∃ (b : Module.Basis (ι ⊕ ι) K V), (toMatrix b) B = Matrix.J ι K ∧ ∀ (i : ι), b (Sum.inl i) = ↑(e i)

Every prescribed basis of a Lagrangian subspace extends to a symplectic basis, with the prescribed vectors as its isotropic half. A Lagrangian is expressed by U = B.orthogonal U; no restriction on the characteristic or on the finite basis index type is needed.