The Iwasawa structure of the symplectic group on projective space

Over a field K, the standard symplectic group Sp_{2m}(K) (TauCeti.GLSymplecticFin m K) acts on the projective space ℙ K (Fin (m + m) → K) through its action on vectors. To a point p of projective space attach the group of symplectic transvections along p,

T(p) = { τ_{v,c} : c ∈ K },        v a nonzero vector on the line p.

It does not depend on the choice of v, because τ_{a v,c} = τ_{v,a²c} and a² ≠ 0. Each T(p) is abelian, being the image of the additive group of K; conjugation by g carries T(p) to T(g p), because g τ_{v,c} g⁻¹ = τ_{g v,c}; and the T(p) generate the symplectic group, because the symplectic transvections do. These are exactly the axioms of Mathlib's MulAction.IwasawaStructure, the data of Iwasawa's simplicity criterion MulAction.IwasawaStructure.isSimpleGroup. This file packages them as TauCeti.GLSymplecticFin.iwasawaStructure.

Applying the criterion to the projective symplectic group needs three further inputs: perfectness of Sp_{2m}(K) (TauCeti.GLSymplecticFin.commutator_eq_top gives it when K has an element a ≠ 0 with a² ≠ 1), quasiprimitivity of the action on projective space, and the identification of the kernel of that action with the centre {±1}. The last two are proved in Symplectic/Primitive and Symplectic/Projective, and Symplectic/Simple assembles the criterion.

Main declarations

• TauCeti.GLSymplecticFin.transvectionSubgroup: the subgroup T(p) of transvections along p, with TauCeti.GLSymplecticFin.transvectionSubgroup_mk computing it from any representative.
• TauCeti.GLSymplecticFin.transvectionSubgroup_smul: T(g p) = g T(p) g⁻¹.
• TauCeti.GLSymplecticFin.iSup_transvectionSubgroup: the T(p) generate Sp_{2m}(K).
• TauCeti.GLSymplecticFin.iwasawaStructure: the resulting Iwasawa structure.

References

• K. Iwasawa, Über die Einfachheit der speziellen projektiven Gruppen, Proc. Imp. Acad. Tokyo 17 (1941), 57--59.
• E. Artin, Geometric Algebra (1957), Chapter III, §§4--5, and Chapter IV, §1.
• D. E. Taylor, The Geometry of the Classical Groups (1992), Chapter 8.

noncomputable def TauCeti.GLSymplecticFin.transvectionSubgroup {K : Type u} [Field K] {m : ℕ} (p : Projectivization K (Fin (m + m) → K)) : Subgroup ↥(GLSymplecticFin m K)

The symplectic transvections along a point p of projective space: the group of transvections τ_{v,c} along a nonzero vector v on the line p. It does not depend on the choice of v (TauCeti.GLSymplecticFin.transvectionSubgroup_mk).

theorem TauCeti.GLSymplecticFin.transvectionSubgroup_mk {K : Type u} [Field K] {m : ℕ} {v : Fin (m + m) → K} (hv : v ≠ 0) : transvectionSubgroup (Projectivization.mk K v hv) = (symplecticTransvectionHom v).range

The transvection group along the point of a nonzero vector v consists of the transvections along v.

@[simp]

theorem TauCeti.GLSymplecticFin.mem_transvectionSubgroup_mk {K : Type u} [Field K] {m : ℕ} {v : Fin (m + m) → K} (hv : v ≠ 0) {g : ↥(GLSymplecticFin m K)} : g ∈ transvectionSubgroup (Projectivization.mk K v hv) ↔ ∃ (c : K), symplecticTransvection v c = g

An element lies in the transvection group along the point of a nonzero vector v exactly when it is a transvection along v.

instance TauCeti.GLSymplecticFin.instIsMulCommutativeSubtypeGeneralLinearGroupFinHAddNatMemSubgroupTransvectionSubgroup {K : Type u} [Field K] {m : ℕ} (p : Projectivization K (Fin (m + m) → K)) : IsMulCommutative ↥(transvectionSubgroup p)

Each transvection group is abelian, being the image of the additive group of the field.

theorem TauCeti.GLSymplecticFin.transvectionSubgroup_smul {K : Type u} [Field K] {m : ℕ} (g : ↥(GLSymplecticFin m K)) (p : Projectivization K (Fin (m + m) → K)) : transvectionSubgroup (g • p) = MulAut.conj g • transvectionSubgroup p

Conjugation moves transvection groups along the action: T(g p) = g T(p) g⁻¹.

theorem TauCeti.GLSymplecticFin.iSup_transvectionSubgroup {K : Type u} [Field K] {m : ℕ} : ⨆ (p : Projectivization K (Fin (m + m) → K)), transvectionSubgroup p = ⊤

The transvection groups generate the symplectic group over a field.

noncomputable def TauCeti.GLSymplecticFin.iwasawaStructure {K : Type u} [Field K] {m : ℕ} : MulAction.IwasawaStructure (↥(GLSymplecticFin m K)) (Projectivization K (Fin (m + m) → K))

The Iwasawa structure of the symplectic group on projective space: the groups of symplectic transvections along the points of ℙ K (Fin (m + m) → K) are abelian, permuted by conjugation compatibly with the action, and generate Sp_{2m}(K).

@[simp]

theorem TauCeti.GLSymplecticFin.iwasawaStructure_T {K : Type u} [Field K] {m : ℕ} (p : Projectivization K (Fin (m + m) → K)) : iwasawaStructure.T p = transvectionSubgroup p

The subgroups of the symplectic Iwasawa structure are the transvection groups.