From a89db3c7832e3b4ed3f64e243f062fc3b8d7441c Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 5 Aug 2026 09:10:50 +0000 Subject: [PATCH] refactor: drop the non-abelian hypothesis from Schreier's conjecture MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Schreier's conjecture is usually stated for non-abelian simple groups, but the hypothesis is not needed for the form the eval problem uses. A finite abelian simple group is `ZMod p`, so its inner automorphisms are trivial and `Out(S) ≅ Aut(S) ≅ (ZMod p)ˣ` is cyclic, hence solvable. Reported by Boris Alexeev, who verified the abelian case in Lean: https://leanprover.zulipchat.com/#narrow/channel/583339-AI-authored-projects/topic/Formalized.20statement.20of.20CFSG.3F/near/614674159 Co-Authored-By: Claude Opus 5 (1M context) Claude-Session: https://claude.ai/code/session_01SpyUgHsbCsg35UDUYUxdiY --- LeanEval/GroupTheory/SchreierConjecture.lean | 10 +++++++--- manifests/problems/schreier_conjecture.toml | 4 ++-- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/LeanEval/GroupTheory/SchreierConjecture.lean b/LeanEval/GroupTheory/SchreierConjecture.lean index d01632d6..f2590ec4 100644 --- a/LeanEval/GroupTheory/SchreierConjecture.lean +++ b/LeanEval/GroupTheory/SchreierConjecture.lean @@ -7,7 +7,7 @@ namespace GroupTheory /-! Schreier's conjecture (theorem, modulo CFSG). -For every finite non-abelian simple group `S`, the outer automorphism group +For every finite simple group `S`, the outer automorphism group `Out(S) := Aut(S) / Inn(S)` is solvable. This was conjectured by Schreier in the 1920s. It is verified case-by-case @@ -15,6 +15,11 @@ through the classification of finite simple groups: for each family (alternating, classical, exceptional Lie type, sporadic) one inspects `Out(S)` and observes solvability. No CFSG-free proof is known. +Schreier's conjecture is usually stated for non-abelian `S`, but that +hypothesis is unnecessary. A finite abelian simple group is `ZMod p`, so its +inner automorphisms are trivial and `Out(S) ≅ Aut(S) ≅ (ZMod p)ˣ` is cyclic, +hence solvable. + `MulAut.conj : S →* MulAut S` sends `s ↦ (conjugation by s)`; its range is `Inn(S)`. The instance below records that `Inn(S)` is normal in `Aut(S)`, which is needed to form the quotient. @@ -32,8 +37,7 @@ instance innNormal (S : Type*) [Group S] : @[eval_problem] theorem schreier_conjecture - (S : Type) [Group S] [Fintype S] [IsSimpleGroup S] - (hS : ∃ a b : S, ¬ Commute a b) : + (S : Type) [Group S] [Fintype S] [IsSimpleGroup S] : IsSolvable (MulAut S ⧸ (MulAut.conj : S →* MulAut S).range) := by sorry diff --git a/manifests/problems/schreier_conjecture.toml b/manifests/problems/schreier_conjecture.toml index a48b11eb..1f948a02 100644 --- a/manifests/problems/schreier_conjecture.toml +++ b/manifests/problems/schreier_conjecture.toml @@ -4,6 +4,6 @@ test = false module = "LeanEval.GroupTheory.SchreierConjecture" holes = ["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." +notes = "For every finite 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. Schreier's conjecture is usually stated for non-abelian S, but that hypothesis is unnecessary: a finite abelian simple group is ZMod p, whose inner automorphisms are trivial and whose automorphism group (ZMod p)ˣ is cyclic, hence solvable." 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." +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. The abelian case needs no classification: S ≅ ZMod p, so Inn(S) is trivial and Out(S) ≅ (ZMod p)ˣ is cyclic."