The Suzuki fixed points are generated by the standard matrices

Over the generator field 𝔽_q, q = 2^(2m+1), the Steinberg fixed points of a valid Suzuki index are the matrices g ∈ Sp₄(𝔽_q) whose special isogeny is the entrywise θ-th power, θ = 2^(m+1): TauCeti.SuzukiLieIndex.finiteFixedSubgroup. This file proves that this subgroup is exactly TauCeti.suzukiGroup m, the group generated by the standard lower unitriangular matrices u(a, b) and the antidiagonal Weyl element w.

The argument is the Bruhat decomposition of the fixed group with respect to the point ∞ = [e₃] of projective three-space, read off the matrix equations. Writing g ∈ H for a fixed point and looking at its last column g e₃:

• if g fixes ∞, the isogeny equations force g to be lower triangular with diagonal (κ, κ^θ / κ, κ / κ^θ, κ⁻¹), so g is the torus element h(κ) of TauCeti.GroupTheory.SpecificGroups.CFSG.Suzuki.Torus times a lower unitriangular fixed point, and a lower unitriangular fixed point is one of the generators u(a, b);
• otherwise the top entry of g e₃ is nonzero, and one generator u(a, b) moves g e₃ onto the line through e₀, where it must in fact lie: for a fixed point whose last column is (z, 0, 0, c) with c ≠ 0, the equations give z = 0. Then w u g fixes ∞.

Both halves only use the equations in the generator coordinates, which the earlier field descent TauCeti.SuzukiLieIndex.mem_finiteFixedSubgroup_iff pulls back from the algebraic closure.

Main results

• TauCeti.SuzukiLieIndex.apply_one_three_eq_zero, apply_two_three_eq_zero and apply_zero_three_eq_zero: the last column of a fixed point is a multiple of e₃ as soon as its top entry vanishes, and conversely when its middle entries vanish and its bottom entry does not.
• TauCeti.SuzukiLieIndex.exists_eq_torus_mul_unipotent: a fixed point fixing ∞ is a torus element times a standard unipotent generator.
• TauCeti.SuzukiLieIndex.exists_eq_unipotent_mul_weyl_mul_torus_mul_unipotent: any other fixed point lies in the big Bruhat cell U w H U.
• TauCeti.SuzukiLieIndex.finiteFixedSubgroup_eq_suzukiGroup: the finite-field fixed subgroup is the generated Suzuki group.
• TauCeti.SuzukiLieIndex.suzukiGroupEquivFixedPoints: the generated Suzuki group is isomorphic to the Steinberg fixed points of the corresponding valid Suzuki index.

Nothing here concerns the derived subgroup or the centre of the fixed points, so no comparison with the candidate group TauCeti.SuzukiLieIndex.Group is made.

References

• M. Suzuki, On a class of doubly transitive groups, Annals of Mathematics 75 (1962), 105--145.
• R. A. Wilson, The Finite Simple Groups, Springer GTM 251 (2009), §4.2, for the matrix generators, the torus, and the point ∞ of the ovoid.

The fixed-point equations over the generator field

The stabiliser of the point at infinity

theorem TauCeti.SuzukiLieIndex.apply_one_three_eq_zero {m : ℕ} {hvalid : (LieTypeIndex.suzuki m).Valid} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ finiteFixedSubgroup m hvalid) (h : ↑g 0 3 = 0) : ↑g 1 3 = 0

A fixed point whose last column has vanishing top entry has vanishing second entry: the isogeny equations at the pairs (0,1), (3,2) and (0,2), (3,2) give g₀₂ g₁₃ = 0 and g₀₂ g₂₃ = g₁₃^θ.

theorem TauCeti.SuzukiLieIndex.apply_two_three_eq_zero {m : ℕ} {hvalid : (LieTypeIndex.suzuki m).Valid} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ finiteFixedSubgroup m hvalid) (h : ↑g 0 3 = 0) : ↑g 2 3 = 0

A fixed point whose last column has vanishing top entry has vanishing third entry.

theorem TauCeti.SuzukiLieIndex.apply_zero_three_eq_zero {m : ℕ} {hvalid : (LieTypeIndex.suzuki m).Valid} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ finiteFixedSubgroup m hvalid) (h1 : ↑g 1 3 = 0) (h2 : ↑g 2 3 = 0) (h3 : ↑g 3 3 ≠ 0) : ↑g 0 3 = 0

A fixed point whose last column is (z, 0, 0, c) with c ≠ 0 has z = 0: the isogeny equations at the pairs (3,2), (3,2) and (0,2), (3,2) give c g₂₂ = c^θ and z g₂₂ = 0.

theorem TauCeti.SuzukiLieIndex.eq_unipotent_of_apply_zero_zero_eq_one {m : ℕ} {hvalid : (LieTypeIndex.suzuki m).Valid} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ finiteFixedSubgroup m hvalid) (h00 : ↑g 0 0 = 1) (h03 : ↑g 0 3 = 0) : g = Suzuki.unipotent m (↑g 1 0) (↑g 3 1)

A fixed point fixing the point at infinity with top-left entry 1 is a standard unipotent generator, namely u(g₁₀, g₃₁).

theorem TauCeti.SuzukiLieIndex.exists_eq_torus_mul_unipotent {m : ℕ} {hvalid : (LieTypeIndex.suzuki m).Valid} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ finiteFixedSubgroup m hvalid) (h : ↑g 0 3 = 0) : ∃ (κ : (GaloisField 2 (2 * m + 1))ˣ) (a : GaloisField 2 (2 * m + 1)) (b : GaloisField 2 (2 * m + 1)), g = (Suzuki.torus m) κ * Suzuki.unipotent m a b

The stabiliser of the point at infinity: a fixed point fixing ∞ is a torus element times a standard unipotent generator.

theorem TauCeti.SuzukiLieIndex.exists_eq_unipotent_mul_weyl_mul_torus_mul_unipotent {m : ℕ} {hvalid : (LieTypeIndex.suzuki m).Valid} {g : GL (Fin 4) (GaloisField 2 (2 * m + 1))} (hg : g ∈ finiteFixedSubgroup m hvalid) (h : ↑g 0 3 ≠ 0) : ∃ (a : GaloisField 2 (2 * m + 1)) (b : GaloisField 2 (2 * m + 1)) (κ : (GaloisField 2 (2 * m + 1))ˣ) (c : GaloisField 2 (2 * m + 1)) (d : GaloisField 2 (2 * m + 1)), g = Suzuki.unipotent m a b * Suzuki.weyl m * ((Suzuki.torus m) κ * Suzuki.unipotent m c d)

The big Bruhat cell: a fixed point not fixing the point at infinity is u(a, b) w h(κ) u(c, d) for standard unipotent generators, the Weyl generator and a torus element.

The generation theorem

theorem TauCeti.SuzukiLieIndex.finiteFixedSubgroup_le_suzukiGroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : finiteFixedSubgroup m hvalid ≤ suzukiGroup m

The finite-field generation theorem: every Steinberg fixed point over the generator field is a product of the standard generators. A fixed point fixing ∞ is a torus element times a unipotent generator, and any other is carried to one by w u(a, b) for the unipotent generator moving its last column onto the line through e₀.

theorem TauCeti.SuzukiLieIndex.finiteFixedSubgroup_eq_suzukiGroup (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : finiteFixedSubgroup m hvalid = suzukiGroup m

The finite-field preimage of the Suzuki Steinberg fixed points is the generated Suzuki group.

noncomputable def TauCeti.SuzukiLieIndex.suzukiGroupEquivFixedPoints (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : ↥(suzukiGroup m) ≃* (of m hvalid).FixedPoints

The generated Suzuki group is the Steinberg fixed-point group: scalar extension along the generator embedding, after the coordinate change, identifies suzukiGroup m with the fixed points of the Steinberg endomorphism of the valid Suzuki index at parameter m.

@[simp]

theorem TauCeti.SuzukiLieIndex.coe_coe_suzukiGroupEquivFixedPoints_apply (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) (g : ↥(suzukiGroup m)) : ↑↑((suzukiGroupEquivFixedPoints m hvalid) g) = (generatorEmbedding m hvalid) ↑g

The identification of the generated Suzuki group with the Steinberg fixed points is, on underlying matrices, the scalar extension of the generator model.