Transitivity of the symplectic group

Over any field, any two nonzero vectors in the standard symplectic space are connected by a product of two symplectic transvections. If their pairing is nonzero, one transvection suffices: use the direction y - x and the inverse of the pairing of y with x. In general, a vector outside the two orthogonal hyperplanes provides an intermediate point. This argument works also over the field with two elements and in rank one.

Consequently Sp₂ₘ acts transitively on projective points. This supplies transitivity for the projective action whose point stabilizers and transvection subgroups enter the simplicity criterion; primitivity is a separate assertion. The vector theorem retains the explicit bound of two transvections, rather than only asserting existence of a symplectic matrix.

References

• E. Artin, Geometric Algebra (1957), Chapter III, §§4--5.
• D. E. Taylor, The Geometry of the Classical Groups (1992), Chapter 8.

The transvections and their vector-action formula are those of TauCeti.GLSymplecticFin.symplecticTransvection.

theorem TauCeti.GLSymplecticFin.coe_symplecticTransvection_sub_mulVec {m : ℕ} {K : Type u} [Field K] {x y : Fin (m + m) → K} (hxy : y ⬝ᵥ (JFin m K).mulVec x ≠ 0) : (↑↑(symplecticTransvection (y - x) (y ⬝ᵥ (JFin m K).mulVec x)⁻¹)).mulVec x = y

When ω(y,x) ≠ 0, the transvection along y - x with parameter ω(y,x)⁻¹ sends x to y.

theorem TauCeti.GLSymplecticFin.exists_symplecticTransvection_mul_mulVec_eq {m : ℕ} {K : Type u} [Field K] {x y : Fin (m + m) → K} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (v : Fin (m + m) → K) (w : Fin (m + m) → K) (a : K) (b : K), (↑↑(symplecticTransvection v a * symplecticTransvection w b)).mulVec x = y

Any two nonzero vectors are connected by a product of at most two symplectic transvections, over every field.

theorem TauCeti.GLSymplecticFin.exists_mulVec_eq {m : ℕ} {K : Type u} [Field K] {x y : Fin (m + m) → K} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (g : ↥(GLSymplecticFin m K)), (↑↑g).mulVec x = y

The standard symplectic group sends any nonzero vector to any other nonzero vector.

theorem TauCeti.GLSymplecticFin.smul_mk_eq_mk_of_mulVec_eq {m : ℕ} {K : Type u} [Field K] {g : ↥(GLSymplecticFin m K)} {x y : Fin (m + m) → K} (hx : x ≠ 0) (hy : y ≠ 0) (h : (↑↑g).mulVec x = y) : g • Projectivization.mk K x hx = Projectivization.mk K y hy

A symplectic matrix sending x to y sends the projective point of x to that of y.

instance TauCeti.GLSymplecticFin.instIsPretransitiveSubtypeGeneralLinearGroupFinHAddNatMemSubgroupProjectivizationForall {m : ℕ} {K : Type u} [Field K] : MulAction.IsPretransitive (↥(GLSymplecticFin m K)) (Projectivization K (Fin (m + m) → K))

The symplectic group acts transitively on projective points, in every rank and over every field. In rank zero the projective space is empty.