Bender–Suzuki theorem

6 fully proved1 ready to prove

Definitions

DefinitionStrongly embedded subgroups#✓fully proved

A subgroup \(M\) of a group \(X\) is strongly embedded in \(X\) if \(M \ne X\), the order of \(M\) is even, and for every \(g \in X\) outside \(M\) the order of \(M \cap g M g^{-1}\) is odd. Here an infinite group is assigned order \(0\), so an infinite \(M\) counts as having even order and an infinite intersection never has odd order.

def IsStronglyEmbedded {X : Type u} [Group X] (M : Subgroup X) : Prop :=
  M ≠ ⊤ ∧ Even (Nat.card M) ∧
    ∀ g ∉ M, Odd (Nat.card ((M ⊓ M.map (MulAut.conj g).toMonoidHom : Subgroup X)))

Used by 1

Used byBender–Suzuki theorem

AbbreviationThe group \(\mathrm{PSL}(2, 2^n)\)#✓fully proved

For a natural number \(n \ge 1\), \(\mathrm{PSL}(2, 2^n)\) is the projective special linear group of \(2 \times 2\) matrices over the Galois field \(\mathrm{GF}(2^n)\). For \(n = 0\) the same construction is taken over \(\mathrm{GF}(2)\) instead.

abbrev PSL2Model (n : ℕ) := ProjectiveSpecialLinearGroup (Fin 2) (GaloisField 2 n)

Used by 1

Used bySimple Bender groups

DefinitionGenerators of the Suzuki group#✓fully proved

Let \(n\) be a natural number, \(q = 2^{2n+1}\), \(\theta = 2^{n+1}\) and \(F = \mathrm{GF}(q)\). The generating set of \(\mathrm{Sz}(q)\) is the set of \(4 \times 4\) matrices over \(F\) of the following three kinds: for \(a, b \in F\), the root element with rows \((1, a, b, a^{2+\theta} + ab + b^{\theta})\), \((0, 1, a^{\theta}, a^{1+\theta} + b)\), \((0, 0, 1, a)\) and \((0, 0, 0, 1)\); for nonzero \(x \in F\), the torus element with diagonal entries \(x^{1+2^n}\), \(x^{2^n}\), \(x^{-2^n}\), \(x^{-(1+2^n)}\) and zeros elsewhere; and the Weyl element, the matrix with ones on the antidiagonal and zeros elsewhere.

The map \(z \mapsto z^{\theta}\) is the Tits automorphism of \(F\): its square is \(z \mapsto z^2\).

def SzGenerators (n : ℕ) : Set (Matrix (Fin 4) (Fin 4) (GaloisField 2 (2 * n + 1))) :=
  {M | (∃ a b, M = !![1, a, b, a ^ (2 + 2 ^ (n + 1)) + a * b + b ^ (2 ^ (n + 1));
                      0, 1, a ^ (2 ^ (n + 1)), a ^ (1 + 2 ^ (n + 1)) + b;
                      0, 0, 1, a;
                      0, 0, 0, 1]) ∨
       (∃ x : (GaloisField 2 (2 * n + 1))ˣ,
          M = !![(x : GaloisField 2 (2 * n + 1)) ^ (1 + 2 ^ n), 0, 0, 0;
                 0, (x : GaloisField 2 (2 * n + 1)) ^ (2 ^ n), 0, 0;
                 0, 0, ((x : GaloisField 2 (2 * n + 1)) ^ (2 ^ n))⁻¹, 0;
                 0, 0, 0, ((x : GaloisField 2 (2 * n + 1)) ^ (1 + 2 ^ n))⁻¹]) ∨
       M = !![0, 0, 0, 1; 0, 0, 1, 0; 0, 1, 0, 0; 1, 0, 0, 0]}

Used by 1

Used byThe Suzuki group \(\mathrm{Sz}(2^{2n+1})\)

DefinitionThe Suzuki group \(\mathrm{Sz}(2^{2n+1})\)#✓fully proved

For a natural number \(n\), the Suzuki group \(\mathrm{Sz}(2^{2n+1})\) is the subgroup of \(\mathrm{GL}(4, \mathrm{GF}(2^{2n+1}))\) generated by the matrices in the generating set of the Suzuki group (all of which are invertible).

noncomputable def SzModel (n : ℕ) : Subgroup (GL (Fin 4) (GaloisField 2 (2 * n + 1))) :=
  Subgroup.closure {A | (A : Matrix (Fin 4) (Fin 4) (GaloisField 2 (2 * n + 1))) ∈
    SzGenerators n}

Uses 1 · Used by 1

Statement usesGenerators of the Suzuki group

Used bySimple Bender groups

DefinitionThe group \(\mathrm{PSU}(3, 2^n)\)#✓fully proved

Let \(n \ge 1\), let \(q = 2^n\) and let \(J\) be the \(3 \times 3\) matrix with ones on the antidiagonal and zeros elsewhere. Then \(\mathrm{PSU}(3, q)\) is the image in the projective general linear group \(\mathrm{PGL}(3, \mathrm{GF}(q^2))\) of the group of matrices \(A \in \mathrm{GL}(3, \mathrm{GF}(q^2))\) with \(\det A = 1\) and \(\bar{A}^{\mathsf{T}} J A = J\), where \(\bar{A}\) is obtained from \(A\) by applying \(z \mapsto z^q\) to every entry. For \(n = 0\) the same construction is taken over \(\mathrm{GF}(2)\) instead, with \(z \mapsto z^q\) the identity.

The map \(z \mapsto z^q\) is the involution of \(\mathrm{GF}(q^2)\) whose fixed field is \(\mathrm{GF}(q)\), so these are the isometries of determinant one of the Hermitian form with Gram matrix \(J\), taken modulo scalars.

noncomputable def PSU3Model (n : ℕ) :
    Subgroup (ProjGenLinGroup (Fin 3) (GaloisField 2 (2 * n))) :=
  (Subgroup.closure {A : GL (Fin 3) (GaloisField 2 (2 * n)) |
      (Matrix.of fun i j =>
          (A : Matrix (Fin 3) (Fin 3) (GaloisField 2 (2 * n))) j i ^ (2 ^ n)) *
        !![0, 0, 1; 0, 1, 0; 1, 0, 0] *
        (A : Matrix (Fin 3) (Fin 3) (GaloisField 2 (2 * n))) =
      !![0, 0, 1; 0, 1, 0; 1, 0, 0] ∧
    GeneralLinearGroup.det A = 1}).map ProjGenLinGroup.mk

Used by 1

Used bySimple Bender groups

InductiveSimple Bender groups#✓fully proved

A group \(G\) is a simple Bender group if it is isomorphic to \(\mathrm{PSL}(2, 2^n)\) for some \(n \ge 2\), to the Suzuki group \(\mathrm{Sz}(2^{2n+1})\) for some \(n \ge 1\), or to \(\mathrm{PSU}(3, 2^n)\) for some \(n \ge 2\).

inductive IsSimpleBenderGroup (G : Type u) [Group G] : Prop
  | isPSL2 (n : ℕ) (_ : 2 ≤ n) (e : G ≃* PSL2Model n)
  | isSuzuki (n : ℕ) (_ : 1 ≤ n) (e : G ≃* SzModel n)
  | isPSU3 (n : ℕ) (_ : 2 ≤ n) (e : G ≃* PSU3Model n)

Uses 3 · Used by 1

Statement usesThe group \(\mathrm{PSL}(2, 2^n)\) · The group \(\mathrm{PSU}(3, 2^n)\) · The Suzuki group \(\mathrm{Sz}(2^{2n+1})\)

Used byBender–Suzuki theorem

Group Theory

TheoremBender–Suzuki theorem#●ready to prove

Let \(X\) be a finite simple group that has a strongly embedded subgroup \(M\). Then \(X\) is a simple Bender group: \(X\) is isomorphic to \(\mathrm{PSL}(2, 2^n)\) for some \(n \ge 2\), to the Suzuki group \(\mathrm{Sz}(2^{2n+1})\) for some \(n \ge 1\), or to \(\mathrm{PSU}(3, 2^n)\) for some \(n \ge 2\).

public theorem_wanted bender_suzuki {X : Type*} [Group X] [Finite X] [IsSimpleGroup X]
    (M : Subgroup X) (h : IsStronglyEmbedded M) :
    IsSimpleBenderGroup X

Sources

• D. Gorenstein, R. Lyons, and R. Solomon, The classification of the finite simple groups, Number 2. Problem bender_suzuki of the lean-eval benchmark.

Uses 2

Statement usesSimple Bender groups · Strongly embedded subgroups

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.