Schreier's conjecture: outer automorphism group of a finite simple group is solvable

schreier_conjecture

Submitter: Kim Morrison.

Notes: For every finite non-abelian simple group S, Out(S) := Aut(S)/Inn(S) is solvable. The statement requires the normality of Inn(S) ⊴ Aut(S), which is supplied by a local instance with a one-line proof (the conjugate of conj(s) by α equals conj(α(s))). Verified case-by-case via CFSG; no CFSG-free proof is known.

Source: O. Schreier, Über die Erweiterung von Gruppen II, Abh. Math. Sem. Univ. Hamburg 4 (1926); CFSG, completed c. 2004.

Informal solution: Use the classification of finite simple groups. For each family — alternating Aₙ, classical Lie type, exceptional Lie type, sporadic — inspect the known Out(S) and verify it is solvable. For Aₙ (n ≥ 5, n ≠ 6), Out = ℤ/2; for A₆, Out = (ℤ/2)²; for groups of Lie type, Out is built from diagonal, field, and graph automorphisms (each step solvable); for sporadics, Out is trivial or ℤ/2.

theorem declaration uses `sorry`schreier_conjecture (S : Type) [Group S] [Fintype S] [IsSimpleGroup S]
    (hS : ∃ a b : S, ¬ Commute a b) :
    IsSolvable (MulAut S ⧸ (MulAut.conj : S →* MulAut S).range) := byS:Typeinst✝²:Group Sinst✝¹:Fintype Sinst✝:IsSimpleGroup ShS:∃ a b, ¬Commute a b⊢ IsSolvable (MulAut S ⧸ MulAut.conj.range)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.