The symplectic group acts primitively on projective space

Let ω(x, y) = xᵀ J y be the standard alternating form on V = Fin (m + m) → K over a field K. The standard symplectic group Sp_{2m}(K) (TauCeti.GLSymplecticFin m K) acts on the projective space ℙ K V. This file proves that the action is primitive; transitivity is the instance in TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Symplectic.Transitivity.

Unlike the special linear group, Sp_{2m}(K) is not doubly transitive on ℙ K V once m ≥ 2: it preserves the relation ω(x, y) = 0 between points. The stabilizer of a point ⟨u⟩ has two orbits on the other points, the points ⟨x⟩ ≠ ⟨u⟩ with ω(u, x) = 0 and those with ω(u, x) ≠ 0. Both orbits are reached by symplectic transvections fixing u: if ω(u, x) = ω(u, y) and ω(y, x) ≠ 0, then the transvection along y - x with parameter ω(y, x)⁻¹ fixes u and sends x to y, and two such steps connect any two vectors x, y off the line of u with ω(u, x) = ω(u, y) (TauCeti.GLSymplecticFin.exists_smul_eq_self_and_smul_eq_of_dotProduct_JFin_mulVec_eq).

A block containing ⟨u⟩ and another point is therefore a union of ⟨u⟩ with whole orbits of the stabilizer. If it contains the points not orthogonal to ⟨u⟩, it also contains a point orthogonal to ⟨u⟩ but not to one of those, and conversely; either way it contains both orbits, so it is the whole space. The argument covers every rank, including m = 1, where no point other than ⟨u⟩ is orthogonal to it.

Primitivity, through MulAction.IsPreprimitive.isQuasiPreprimitive, is the quasiprimitivity input of Iwasawa's simplicity criterion MulAction.IwasawaStructure.isSimpleGroup for the projective symplectic group.

Main results

• TauCeti.GLSymplecticFin.exists_smul_eq_self_and_smul_eq_of_dotProduct_JFin_mulVec_eq: the stabilizer of a vector u moves x to y whenever both lie off the line of u and ω(u, x) = ω(u, y).
• TauCeti.GLSymplecticFin.isPreprimitive: Sp_{2m}(K) acts primitively on ℙ K V.

References

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

theorem TauCeti.GLSymplecticFin.exists_smul_eq_self_and_smul_eq_of_dotProduct_JFin_mulVec_eq {K : Type u} [Field K] {m : ℕ} {u x y : Fin (m + m) → K} (hx : x ∉ K ∙ u) (hy : y ∉ K ∙ u) (h : u ⬝ᵥ (JFin m K).mulVec x = u ⬝ᵥ (JFin m K).mulVec y) : ∃ (g : ↥(GLSymplecticFin m K)), g • u = u ∧ g • x = y

The stabilizer of a vector u is transitive on each level set of ω(u, ·) off the line of u. If neither x nor y is a multiple of u and ω(u, x) = ω(u, y), a product of at most two symplectic transvections fixes u and sends x to y. For u = 0 this is the transitivity of Sp_{2m}(K) on nonzero vectors.

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

The symplectic group acts primitively on projective space. A block containing two points ⟨u⟩ ≠ ⟨x⟩ contains a point orthogonal to ⟨u⟩ and a point not orthogonal to it, hence both orbits of the stabilizer of ⟨u⟩ on the other points, hence everything.