Brauer–Suzuki theorem

1 fully proved1 ready to prove

Definitions

DefinitionOdd core of a group#✓fully proved

The odd core \(O(G)\) of a group \(G\) is the supremum, in the lattice of subgroups of \(G\), of all normal subgroups of \(G\) whose order is finite and odd.

For a finite group this is the largest normal subgroup of odd order, classically denoted \(O(G)\) (in older notation \(O_{2'}(G)\)): the join of two normal subgroups of odd order is again a normal subgroup of odd order, so the supremum is itself one. 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)}

Used by 1

Used byBrauer–Suzuki theorem

Group Theory

TheoremBrauer–Suzuki theorem#●ready to prove

Let \(G\) be a finite group, let \(O(G)\), the odd core of \(G\), be the subgroup generated by all normal subgroups of \(G\) of odd order, let \(n \ge 3\), and let \(P\) be a Sylow \(2\)-subgroup of \(G\) isomorphic to the generalized quaternion group \(Q_{2^n}\) of order \(2^n\). If \(t \in P\) has order \(2\), then the image of \(t\) in \(G / O(G)\) lies in the center of \(G / O(G)\).

public theorem_wanted 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)

Sources

• 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. Problem brauer_suzuki of the lean-eval benchmark.

Uses 1

Statement usesOdd core of a group

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.