Symplectic bases of nondegenerate alternating forms

A nondegenerate alternating bilinear form B on a finite-dimensional vector space V over a field has a symplectic basis: a basis b indexed by Fin m ⊕ Fin m in which the matrix of B is the standard matrix Matrix.J (Fin m) K, so B (b (inr a)) (b (inl a)) = 1, every other pair of basis vectors is orthogonal, and in particular V has even dimension 2 * m.

The theorem is proved in a graded form. Suppose V is spanned by a family of subspaces W : ι → Submodule K V, the index type carries an involution σ, and B pairs W i with W j trivially unless j = σ i. Then the symplectic basis can be chosen to consist of vectors each lying in some W i. The ungraded theorem is the case of a single subspace ⊤. The graded form is what a diagonalizable subgroup of a symplectic group needs: its weight spaces are paired by inversion of characters, and a homogeneous symplectic basis is a symplectic change of coordinates diagonalizing the subgroup.

The proof is the classical induction on dimension. A nonzero homogeneous vector e ∈ W i pairs nontrivially with some homogeneous f ∈ W (σ i), normalized to B f e = 1. The orthogonal complement of span {e, f} has dimension two less, carries a nondegenerate restriction of B, and is spanned by its intersections with the W j, because the projection u ↦ u - B f u • e + B e u • f onto it preserves homogeneity. Adjoining e and f to a homogeneous symplectic basis of the complement gives one of V. The facts about a single hyperbolic pair e, f hold over any commutative ring and are stated at that level.

Main declarations

• LinearMap.BilinForm.IsAlt.restrict_nondegenerate_orthogonal_span_pair: a nondegenerate alternating form stays nondegenerate on the orthogonal complement of a hyperbolic pair.
• LinearMap.BilinForm.IsAlt.exists_basis_apply_eq_J_of_basis_orthogonal_span_pair: adjoining a hyperbolic pair to a symplectic basis of the orthogonal complement of its span gives a symplectic basis.
• LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J_of_iSup_eq_top: a nondegenerate alternating form on a compatibly graded space has a homogeneous symplectic basis.
• LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J: a nondegenerate alternating form has a symplectic basis.
• LinearMap.BilinForm.IsAlt.even_finrank: a space carrying a nondegenerate alternating form has even dimension.
• LinearMap.BilinForm.IsAlt.exists_basis_apply_eq_J_inl_zero_eq: every nonzero vector is the vector at inl 0 of some symplectic basis.

References

• E. Artin, Geometric Algebra (1957), Theorem 3.7.
• S. Lang, Algebra, revised 3rd ed. (2002), Chapter XV, Theorem 8.1.

theorem LinearMap.BilinForm.Nondegenerate.exists_mem_apply_ne_zero_of_iSup_eq_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (hnd : B.Nondegenerate) {ι : Type u_3} {W : ι → Submodule R M} {σ : ι → ι} (hσ : Function.Involutive σ) (hW : ⨆ (i : ι), W i = ⊤) (horth : ∀ (i j : ι), j ≠ σ i → ∀ v ∈ W i, ∀ w ∈ W j, (B v) w = 0) {i : ι} {v : M} (hv : v ∈ W i) (hv0 : v ≠ 0) : ∃ w ∈ W (σ i), (B w) v ≠ 0

In a space spanned by a family of subspaces paired trivially by B except along an involution σ, a nonzero vector of W i pairs nontrivially with some vector of W (σ i).

theorem LinearMap.BilinForm.IsAlt.linearIndependent_pair_of_apply_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsAlt) {e f : M} (hfe : (B f) e = 1) : LinearIndependent R ![e, f]

Two vectors pairing to 1 under an alternating form are linearly independent.

theorem LinearMap.BilinForm.IsAlt.sub_smul_add_smul_mem_orthogonal_span_pair {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsAlt) {e f : M} (hfe : (B f) e = 1) (u : M) : u - (B f) u • e + (B e) u • f ∈ B.orthogonal (Submodule.span R {e, f})

The projection u ↦ u - B f u • e + B e u • f lands in the orthogonal complement of the span of the hyperbolic pair e, f.

theorem LinearMap.BilinForm.IsAlt.restrict_nondegenerate_orthogonal_span_pair {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (hB : B.IsAlt) {e f : M} (hfe : (B f) e = 1) (hnd : B.Nondegenerate) : (B.restrict (B.orthogonal (Submodule.span R {e, f}))).Nondegenerate

The restriction of a nondegenerate alternating form to the orthogonal complement of the span of a hyperbolic pair is nondegenerate.

theorem LinearMap.BilinForm.IsAlt.finrank_orthogonal_span_pair_add_two {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) {e f : V} (hfe : (B f) e = 1) : Module.finrank K ↥(B.orthogonal (Submodule.span K {e, f})) + 2 = Module.finrank K V

The orthogonal complement of the span of a hyperbolic pair has codimension two.

theorem LinearMap.BilinForm.IsAlt.exists_basis_apply_eq_J_of_basis_orthogonal_span_pair {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) {e f : V} (hfe : (B f) e = 1) {m : ℕ} (c : Module.Basis (Fin m ⊕ Fin m) K ↥(B.orthogonal (Submodule.span K {e, f}))) (hc : ∀ (x y : Fin m ⊕ Fin m), (B ↑(c x)) ↑(c y) = Matrix.J (Fin m) K x y) : ∃ (b : Module.Basis (Fin (m + 1) ⊕ Fin (m + 1)) K V), (∀ (x y : Fin (m + 1) ⊕ Fin (m + 1)), (B (b x)) (b y) = Matrix.J (Fin (m + 1)) K x y) ∧ ⇑b = Sum.elim (Fin.cons e fun (a : Fin m) => ↑(c (Sum.inl a))) (Fin.cons f fun (a : Fin m) => ↑(c (Sum.inr a)))

Adjoining a hyperbolic pair to a symplectic basis of the orthogonal complement of its span gives a symplectic basis. The new basis puts e and f in the positions inl 0 and inr 0 and shifts the given basis of the complement to the successor positions.

theorem LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J_of_iSup_eq_top {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) {ι : Type u_3} {W : ι → Submodule K V} {σ : ι → ι} (hσ : Function.Involutive σ) (hW : ⨆ (i : ι), W i = ⊤) (horth : ∀ (i j : ι), j ≠ σ i → ∀ v ∈ W i, ∀ w ∈ W j, (B v) w = 0) : ∃ (m : ℕ) (b : Module.Basis (Fin m ⊕ Fin m) K V), (toMatrix b) B = Matrix.J (Fin m) K ∧ ∀ (x : Fin m ⊕ Fin m), ∃ (i : ι), b x ∈ W i

A nondegenerate alternating form on a compatibly graded space has a homogeneous symplectic basis.

Let V be spanned by subspaces W i, indexed by a type with an involution σ, such that B pairs W i and W j trivially unless j = σ i. Then V has a basis indexed by Fin m ⊕ Fin m in which the matrix of B is the standard symplectic matrix Matrix.J, every vector of which lies in one of the W i.

theorem LinearMap.BilinForm.IsAlt.exists_basis_toMatrix_eq_J {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) : ∃ (m : ℕ) (b : Module.Basis (Fin m ⊕ Fin m) K V), (toMatrix b) B = Matrix.J (Fin m) K

A nondegenerate alternating form has a symplectic basis: a basis indexed by Fin m ⊕ Fin m in which its matrix is the standard symplectic matrix Matrix.J.

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 finite-dimensional space carrying a nondegenerate alternating form has even dimension.

theorem LinearMap.BilinForm.IsAlt.exists_basis_apply_eq_J_inl_zero_eq {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) {e : V} (he : e ≠ 0) : ∃ (m : ℕ) (b : Module.Basis (Fin (m + 1) ⊕ Fin (m + 1)) K V), (∀ (x y : Fin (m + 1) ⊕ Fin (m + 1)), (B (b x)) (b y) = Matrix.J (Fin (m + 1)) K x y) ∧ b (Sum.inl 0) = e

Every nonzero vector heads a symplectic basis. For a nondegenerate alternating form on a finite-dimensional space and a nonzero vector e, there is a basis indexed by Fin (m + 1) ⊕ Fin (m + 1) in which the matrix of the form is Matrix.J and whose vector at the position inl 0 is e.