feat: add Brauer-Suzuki theorem eval problem

LeanEval/GroupTheory/BrauerSuzuki.lean

@@ -0,0 +1,46 @@
+import Mathlib
+import EvalTools.Markers
+import LeanEval.GroupTheory.Defs.OddCore
+
+namespace LeanEval
+namespace GroupTheory
+
+open LeanEval.GroupTheory.Defs
+
+/-!
+# Brauer–Suzuki theorem on generalized quaternion Sylow 2-subgroups
+
+Let `G` be a finite group whose Sylow 2-subgroups are generalized
+quaternion: isomorphic to `Q_{2^n}` for some `n ≥ 3`, i.e., to Mathlib's
+`QuaternionGroup (2^(n-2))` (since `QuaternionGroup m` has order `4m`,
+giving `|Q_{2^n}| = 2^n` and `n = log₂|P|`). Let `t` be the unique
+involution of any (equivalently, every) Sylow 2-subgroup. Then the
+image of `t` in `G / O(G)` is central, where `O(G)` is the largest
+normal subgroup of `G` of odd order.
+
+R. Brauer and M. Suzuki, "On finite groups of even order whose 2-Sylow
+group is a quaternion group", Proc. Nat. Acad. Sci. U.S.A. 45 (1959).
+This was the precursor of Glauberman's Z*-theorem (1966) and the
+historical seed of the local-analysis programme in CFSG.
+
+The conclusion is phrased entirely in the quotient `G / O(G)`,
+applied to the image of `t` under `QuotientGroup.mk`; the value of
+`t : G` only enters via that map.
+
+Introduces `Defs/OddCore.lean` since Mathlib has no `oddCore`/`O(G)`
+operation.
+-/
+
+/-- **Brauer–Suzuki theorem (quaternion case).** -/
+@[eval_problem]
+theorem brauer_suzuki {G : Type*} [Group G] [Finite G]
+    (n : ℕ) (hn : 3 ≤ n)
+    (P : Sylow 2 G)
+    (hquat : Nonempty ((P : Subgroup G) ≃* QuaternionGroup (2 ^ (n - 2))))
+    (t : G) (ht_mem : t ∈ (P : Subgroup G)) (ht_ord : orderOf t = 2) :
+    (QuotientGroup.mk t : G ⧸ oddCore G) ∈
+      Subgroup.center (G ⧸ oddCore G) := by
+  sorry
+
+end GroupTheory
+end LeanEval

LeanEval/GroupTheory/Defs/OddCore.lean

@@ -0,0 +1,45 @@
+import Mathlib
+
+namespace LeanEval
+namespace GroupTheory
+namespace Defs
+
+/-- `oddCore G` is the largest normal subgroup of `G` of odd order — the
+supremum of all normal subgroups whose cardinality is odd. Classically
+denoted `O(G)` (in older notation `O_{2'}(G)`).
+
+For a finite group, the join of two normal odd-order subgroups is again
+a normal odd-order subgroup, and finiteness bounds the chain — so the
+supremum is itself a normal subgroup of odd order, agreeing with the
+textbook definition. For an infinite group the definition still makes
+sense as a subgroup, though it need not be of odd order.
+-/
+def oddCore (G : Type*) [Group G] : Subgroup G :=
+  sSup {N : Subgroup G | N.Normal ∧ Odd (Nat.card N)}
+
+/-- The odd core is normal: conjugation by any `g : G` fixes every normal
+subgroup in the family pointwise, hence fixes their supremum setwise. -/
+instance oddCore_normal (G : Type*) [Group G] : (oddCore G).Normal where
+  conj_mem n hn g := by
+    have hn' : n ∈ ⨆ N : {N : Subgroup G // N.Normal ∧ Odd (Nat.card N)},
+        (N : Subgroup G) := by
+      rwa [oddCore, sSup_eq_iSup'] at hn
+    refine Subgroup.iSup_induction (C := fun y => g * y * g⁻¹ ∈ oddCore G)
+      _ hn' (fun N x hxN => ?_) ?_ (fun x y hx hy => ?_)
+    · -- `N.val` is a normal subgroup, so `g * x * g⁻¹ ∈ N.val ≤ oddCore G`
+      have hN_norm : (N : Subgroup G).Normal := N.prop.1
+      exact (le_sSup N.prop : (N : Subgroup G) ≤ oddCore G)
+        (hN_norm.conj_mem x hxN g)
+    · -- `g * 1 * g⁻¹ = 1 ∈ oddCore G`
+      show g * 1 * g⁻¹ ∈ oddCore G
+      simp
+    · -- `g * (x * y) * g⁻¹ = (g * x * g⁻¹) * (g * y * g⁻¹)`
+      show g * (x * y) * g⁻¹ ∈ oddCore G
+      have h_distr : g * (x * y) * g⁻¹ = (g * x * g⁻¹) * (g * y * g⁻¹) := by
+        group
+      rw [h_distr]
+      exact mul_mem hx hy
+
+end Defs
+end GroupTheory
+end LeanEval

manifests/problems/brauer_suzuki.toml

@@ -0,0 +1,9 @@
+id = "brauer_suzuki"
+title = "Brauer–Suzuki theorem (quaternion Sylow 2-subgroup)"
+test = false
+module = "LeanEval.GroupTheory.BrauerSuzuki"
+holes = ["brauer_suzuki"]
+submitter = "Kim Morrison"
+notes = "If a finite group G has generalized quaternion Sylow 2-subgroups, then the unique involution of G maps to a central element of G/O(G), where O(G) is the largest normal odd-order subgroup. R. Brauer and M. Suzuki, 'On finite groups of even order whose 2-Sylow group is a quaternion group', Proc. Nat. Acad. Sci. U.S.A. 45 (1959), 1757-1759. Historical precursor of Glauberman's Z*-theorem (1966) and the local-analysis programme in CFSG. Introduces Defs/OddCore.lean defining O(G) as the supremum of all normal odd-order subgroups (Mathlib has no `oddCore` operation)."
+source = "R. Brauer and M. Suzuki, On finite groups of even order whose 2-Sylow group is a quaternion group, Proc. Nat. Acad. Sci. U.S.A. 45 (1959), 1757-1759. https://doi.org/10.1073/pnas.45.12.1757"
+informal_solution = "The argument is character-theoretic and proceeds via a careful analysis of the principal 2-block of G. In a generalized quaternion 2-Sylow P, the unique involution z = a^{2^{n-2}} is central in P (where a is the generator of the cyclic maximal subgroup of P). Brauer's principal-block reformulation: z lies in the kernel of every ordinary irreducible character not in the principal 2-block, plus an analysis of how the principal block's characters restrict to ⟨z⟩, forces z·O(G) into the center of G/O(G). Modern simplification: Glauberman's Z*-theorem, of which Brauer-Suzuki is the prototypical case, says any isolated involution is in Z*(G); the unique involution of a generalized-quaternion Sylow 2-subgroup is automatically isolated."