The Suzuki groups are simple

Let q = 2^(2m+1) with m ≠ 0 and let G = Sz(q) be TauCeti.suzukiGroup m, the subgroup of GL₄(𝔽_q) generated by the lower unitriangular matrices u(a, b) and the antidiagonal Weyl element w. This file proves that G is simple, and hence so is the Suzuki candidate group TauCeti.SuzukiLieIndex.Group of every valid Suzuki index.

The proof applies Tits's simplicity theorem to a Tits system of rank one on G:

• U = {u(a, b)} is the unipotent subgroup; its elements satisfy u⁴ = 1, so U is a 2-group and therefore solvable;
• B = H U is the Borel subgroup, the product of the torus H = {h(κ)} and U; the torus normalizes U, so B does;
• N is the group of order two generated by w.

The rank-one Bruhat decomposition G = B ∪ B w B is the content of the generation theorem TauCeti.SuzukiLieIndex.finiteFixedSubgroup_eq_suzukiGroup, whose two cases TauCeti.SuzukiLieIndex.exists_eq_torus_mul_unipotent and TauCeti.SuzukiLieIndex.exists_eq_unipotent_mul_weyl_mul_torus_mul_unipotent put every element in B or in B w B. The conjugate w u(a, b) w lies in B only for u(a, b) = 1, which is the remaining axiom w B w ≠ B. Since G is perfect (TauCeti.Suzuki.isPerfect_suzukiGroup) and the conjugates of U generate G, Tits's theorem shows that every normal subgroup of G is G or lies in the normal core Z of B.

Finally Z is trivial. An element of Z ∩ U is conjugated into B by w, so it is trivial; hence Z, which normalizes U, commutes with U. The centralizer of the normal subgroup Z is normal and contains U, so it is all of G, and Z lies in the centre of G, which is trivial (TauCeti.Suzuki.center_suzukiGroup_eq_bot).

Main definitions and results

The subgroups U and B = H U, TauCeti.Suzuki.unipotentSubgroup and TauCeti.Suzuki.borelSubgroup, are defined in the files on the generators and on the torus.

• TauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset: the Bruhat decomposition Sz(q) = B ∪ B w B.
• TauCeti.Suzuki.titsSystem: the Tits system (B, ⟨w⟩) of rank one on Sz(q), whose only simple reflection is the class of w (TauCeti.Suzuki.titsSystem_simple), so that it is irreducible (TauCeti.Suzuki.isIrreducible_titsSystem).
• TauCeti.Suzuki.normalCore_borelSubgroupOf: the normal core of the Borel subgroup is trivial.
• TauCeti.Suzuki.isSimpleGroup_suzukiGroup: Sz(q) is simple for m ≠ 0.
• TauCeti.SuzukiLieIndex.isSimpleGroup_group: the candidate group of every valid Suzuki index is simple.

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.
• J. E. Humphreys, Linear Algebraic Groups (1975), Section 29.5, for Tits's simplicity theorem.

The Tits system of rank one

theorem TauCeti.Suzuki.mem_borelSubgroupOf_or_mem_doubleCoset (m : ℕ) (hm : m ≠ 0) (g : ↥(suzukiGroup m)) : g ∈ borelSubgroupOf m ∨ g ∈ DoubleCoset.doubleCoset (weylOf m) ↑(borelSubgroupOf m) ↑(borelSubgroupOf m)

The rank-one Bruhat decomposition Sz(q) = B ∪ B w B, for m ≠ 0.

noncomputable def TauCeti.Suzuki.titsSystem (m : ℕ) (hm : m ≠ 0) : TitsSystem ↥(suzukiGroup m)

The Tits system of rank one on Sz(q), for m ≠ 0: B = H U is the Borel subgroup and N is the group of order two generated by the Weyl element w.

@[simp]

theorem TauCeti.Suzuki.titsSystem_subgroupB (m : ℕ) (hm : m ≠ 0) : (titsSystem m hm).subgroupB = borelSubgroupOf m

The subgroup B of the Tits system of Sz(q) is the Borel subgroup.

@[simp]

theorem TauCeti.Suzuki.titsSystem_subgroupN (m : ℕ) (hm : m ≠ 0) : (titsSystem m hm).subgroupN = Subgroup.zpowers (weylOf m)

The subgroup N of the Tits system of Sz(q) is generated by the Weyl element.

@[simp]

theorem TauCeti.Suzuki.titsSystem_simple (m : ℕ) (hm : m ≠ 0) : (titsSystem m hm).simple = {↑⟨weylOf m, ⋯⟩}

The only simple reflection of the Tits system of Sz(q) is the class of the Weyl element.

theorem TauCeti.Suzuki.isIrreducible_titsSystem (m : ℕ) (hm : m ≠ 0) : (titsSystem m hm).IsIrreducible

The Tits system of Sz(q) is irreducible, having a single simple reflection.

Simplicity

theorem TauCeti.Suzuki.normalCore_borelSubgroupOf (m : ℕ) : (borelSubgroupOf m).normalCore = ⊥

The normal core of the Borel subgroup of Sz(q) is trivial.

theorem TauCeti.Suzuki.isSimpleGroup_suzukiGroup (m : ℕ) (hm : m ≠ 0) : IsSimpleGroup ↥(suzukiGroup m)

The Suzuki group Sz(2^(2m+1)) is simple for m ≠ 0.

theorem TauCeti.SuzukiLieIndex.isSimpleGroup_group (m : ℕ) (hvalid : (LieTypeIndex.suzuki m).Valid) : IsSimpleGroup (of m hvalid).Group

The candidate group of every valid Suzuki index is simple: it is the generated Suzuki group Sz(2^(2m+1)), and validity forces m ≠ 0.