The faithful projective action of the symplectic group

The kernel of the action of Sp₂ₘ(K) on projective points is precisely its center. Thus the quotient by the center acts faithfully on the same projective space, in every characteristic. This supplies the faithful action used in simplicity criteria for projective symplectic groups; primitivity and perfectness are separate requirements.

The quotient action follows Mathlib's Projectivization.PSLAction.toPermHom construction for the special linear group. The center calculation is the one in Symplectic/Center.

References

• D. E. Taylor, The Geometry of the Classical Groups, Chapter 8.

theorem TauCeti.GLSymplecticFin.forall_projective_smul_eq_iff_mem_center {m : ℕ} {K : Type u_1} [Field K] (g : ↥(GLSymplecticFin m K)) : (∀ (p : Projectivization K (Fin (m + m) → K)), g • p = p) ↔ g ∈ Subgroup.center ↥(GLSymplecticFin m K)

A symplectic element fixes every projective point exactly when it is central.

theorem TauCeti.GLSymplecticFin.ker_projective_toPermHom {m : ℕ} {K : Type u_1} [Field K] : (MulAction.toPermHom (↥(GLSymplecticFin m K)) (Projectivization K (Fin (m + m) → K))).ker = Subgroup.center ↥(GLSymplecticFin m K)

The permutation action on projective points has exactly the symplectic center as kernel.

def TauCeti.GLSymplecticFin.projectiveToPermHom {m : ℕ} {K : Type u_1} [Field K] : ↥(GLSymplecticFin m K) ⧸ Subgroup.center ↥(GLSymplecticFin m K) →* Equiv.Perm (Projectivization K (Fin (m + m) → K))

The symplectic action on projective space, factored through the quotient by its center.

@[simp]

theorem TauCeti.GLSymplecticFin.projectiveToPermHom_mk {m : ℕ} {K : Type u_1} [Field K] (g : ↥(GLSymplecticFin m K)) : projectiveToPermHom ↑g = (MulAction.toPermHom (↥(GLSymplecticFin m K)) (Projectivization K (Fin (m + m) → K))) g

On a represented coset, the projective permutation is the original symplectic action.

@[instance_reducible]

instance TauCeti.GLSymplecticFin.instMulActionQuotientSubtypeGeneralLinearGroupFinHAddNatMemSubgroupCenterProjectivizationForall {m : ℕ} {K : Type u_1} [Field K] : MulAction (↥(GLSymplecticFin m K) ⧸ Subgroup.center ↥(GLSymplecticFin m K)) (Projectivization K (Fin (m + m) → K))

@[simp]

theorem TauCeti.GLSymplecticFin.quotient_center_mk_smul {m : ℕ} {K : Type u_1} [Field K] (g : ↥(GLSymplecticFin m K)) (p : Projectivization K (Fin (m + m) → K)) : ↑g • p = g • p

Quotienting by the center does not change how a symplectic element acts on a line.

theorem TauCeti.GLSymplecticFin.projectiveToPermHom_injective {m : ℕ} {K : Type u_1} [Field K] : Function.Injective ⇑projectiveToPermHom

The projective permutation representation of the central quotient is injective.

instance TauCeti.GLSymplecticFin.instFaithfulSMulQuotientSubtypeGeneralLinearGroupFinHAddNatMemSubgroupCenterProjectivizationForall {m : ℕ} {K : Type u_1} [Field K] : FaithfulSMul (↥(GLSymplecticFin m K) ⧸ Subgroup.center ↥(GLSymplecticFin m K)) (Projectivization K (Fin (m + m) → K))