The centre of a Suzuki group

TauCeti.suzukiGroup n is the subgroup of GL₄(𝔽_(2^(2n+1))) generated by the unipotent matrices u(a, b) and the Weyl matrix w. This file proves that its centre is trivial. The determinant-one calculations for the generators show that every group element has determinant one. A separate linear-algebra computation shows that already the three generators u(1, 0), u(0, 1) and w have scalar commutant, so a matrix commuting with them is a multiple of the identity. A central element of the Suzuki group is therefore a scalar c with c ^ 4 = 1, and (c - 1) ^ 4 = c ^ 4 - 1 in characteristic two, so c = 1.

Triviality of the centre is one of the two hypotheses of TauCeti.DerivedCentralQuotient.mulEquivOfCenterEqBot, which identifies a perfect group with trivial centre with its own derived central quotient. The other hypothesis, perfectness, is not proved here, and neither simplicity nor the order of the group is asserted.

Main results

• TauCeti.Suzuki.eq_smul_one_of_commute: a four-by-four matrix commuting with u(1, 0), u(0, 1) and w is a scalar multiple of the identity matrix.
• TauCeti.Suzuki.center_suzukiGroup_eq_bot: the centre of a Suzuki group is trivial, at every parameter, including n = 0, where the group is the solvable group Sz(2).

References

• M. Suzuki, On a class of doubly transitive groups, Annals of Mathematics 75 (1962), 105--145, for the generating matrices.

theorem TauCeti.Suzuki.eq_smul_one_of_commute (n : ℕ) {M : Matrix (Fin 4) (Fin 4) (GaloisField 2 (2 * n + 1))} (h₁ : Commute M (unipotentMatrix n 1 0)) (h₂ : Commute M (unipotentMatrix n 0 1)) (hw : Commute M (weylMatrix n)) : M = M 0 0 • 1

A matrix commuting with the generators u(1, 0), u(0, 1) and w is scalar. Three of the generators of a Suzuki group already have scalar commutant in the full matrix algebra, so in particular the centralizer of a Suzuki group consists of scalar matrices.

@[simp]

theorem TauCeti.Suzuki.center_suzukiGroup_eq_bot (n : ℕ) : Subgroup.center ↥(suzukiGroup n) = ⊥

The centre of a Suzuki group is trivial. This holds at every parameter, including n = 0, where the group is the solvable group Sz(2).