Finite simple groups and involutions

Finite simple and almost simple groups and the local analysis behind their classification: specific simple groups (Mathieu, Suzuki, PSL), strongly embedded subgroups (Bender–Suzuki), classification by Sylow 2-subgroups (Gorenstein–Walter, Brauer–Suzuki), Baer–Suzuki, Glauberman Z*, Brauer–Fowler, involution centralizers and 3-transpositions; generation questions go to Generation of groups and spectrum recognition to Group orders, element orders and spectra.

• 3-transposition groups
• Baer–Suzuki theorem
• Bender–Suzuki theorem
• Brauer–Suzuki theorem
• Glauberman Z*-theorem
• Involution centralizers
• Mathieu group M₂₃

TheoremBrauer–Fowler theorem#●ready to prove

There is a function \(f \colon \mathbb{N} \to \mathbb{N}\) such that for every finite nonabelian simple group \(G\) and every element \(t \in G\) of order \(2\), with centralizer \(C_G(t)\) in \(G\), the order of \(G\) satisfies \(|G| \le f(|C_G(t)|)\).

public theorem_wanted brauer_fowler :
    ∃ f : ℕ → ℕ, ∀ (G : Type) [Group G] [Finite G],
      IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
      ∀ t : G, orderOf t = 2 →
        Nat.card G ≤ f (Nat.card (Subgroup.centralizer ({t} : Set G)))

Sources

• R. Brauer and K. A. Fowler, On groups of even order, Ann. of Math. (2) 62 (1955), 565-583. https://doi.org/10.2307/1970080. Problem brauer_fowler of the lean-eval benchmark.

TheoremGorenstein–Walter theorem#●ready to prove

Let \(G\) be a finite nonabelian simple group, and let \(P\) be a Sylow \(2\)-subgroup of \(G\) that is isomorphic to the dihedral group \(D_n\) for some natural number \(n\) (of order \(2n\) when \(n \ge 1\); \(D_0\) is the infinite dihedral group). Then \(G\) is isomorphic to the alternating group \(A_7\), or to the projective special linear group \(\mathrm{PSL}_2(\mathbb{F}_q)\) for some power \(q = p^k\) of an odd prime \(p\) with \(q \ge 5\).

public theorem_wanted gorenstein_walter
    (G : Type) [Group G] [Finite G] [IsSimpleGroup G]
    (hnonab : ∃ a b : G, a * b ≠ b * a)
    (P : Sylow 2 G)
    (_hdih : ∃ n : ℕ, Nonempty ((P : Subgroup G) ≃* DihedralGroup n)) :
    Nonempty (G ≃* alternatingGroup (Fin 7)) ∨
    ∃ p k : ℕ, ∃ _hp : Fact p.Prime, Odd p ∧ 5 ≤ p ^ k ∧
      (letI := _hp; Nonempty (G ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) (GaloisField p k)))

Sources

• D. Gorenstein and J. H. Walter, The characterization of finite groups with dihedral Sylow 2-subgroups, J. Algebra 2 (1965), 85-151, 218-270, 354-393. https://doi.org/10.1016/0021-8693(65)90027-X. Problem gorenstein_walter of the lean-eval benchmark.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.