Glauberman Z*-theorem

TheoremGlauberman's \(Z^*\)-theorem#●ready to prove

Glauberman's \(Z^*\)-theorem. Let \(G\) be a finite group and let \(t \in G\) be an involution (\(t \neq 1\) and \(t^2 = 1\)) such that every conjugate \(g t g^{-1}\) of \(t\) that commutes with \(t\) equals \(t\). Then there is a normal subgroup \(N\) of \(G\) of odd order such that \(g t g^{-1} t^{-1} \in N\) for every \(g \in G\).

public theorem_wanted glauberman_zStar
    (G : Type) [Group G] [Fintype G]
    (t : G) (ht1 : t ≠ 1) (ht2 : t * t = 1)
    (hisolated : ∀ g : G, (g * t * g⁻¹) * t = t * (g * t * g⁻¹) →
      g * t * g⁻¹ = t) :
    ∃ N : Subgroup G, N.Normal ∧ Odd (Nat.card N) ∧
      ∀ g : G, g * t * g⁻¹ * t⁻¹ ∈ N

Sources

• G. Glauberman, Central elements in core-free groups, J. Algebra 4 (1966). Problem glauberman_zStar of the lean-eval benchmark.

DefinitionOdd core from normal subgroups of odd-order elements#✓fully proved

For a group \(G\), \(O(G)\) is the join, in the lattice of subgroups of \(G\), of all normal subgroups \(N\) of \(G\) such that every element of \(N\) has finite odd order. In a periodic group this join is again a normal subgroup consisting of elements of odd order, so it is the largest such subgroup.

def oddCore (G : Type*) [Group G] : Subgroup G :=
  sSup {N : Subgroup G | N.Normal ∧ ∀ x ∈ N, Odd (orderOf x)}

Used by 1

Used byBorovik's question on involutions with odd-order products (Kourovka 11.13)

DefinitionBorovik's question on involutions with odd-order products (Kourovka 11.13)#✓fully proved

For a group \(G\), let \(O(G)\) be the join of all normal subgroups of \(G\) all of whose elements have odd order. This is the statement that for every periodic group \(G\) and every involution \(i \in G\) such that \(g^{-1} i g i\) has odd order for every \(g \in G\), the image of \(i\) in \(G / O(G)\) is central, that is, \(g i g^{-1} i^{-1} \in O(G)\) for every \(g \in G\).

def periodicInvolutionCentralModOddCore : Prop :=
  ∀ (G : Type) [Group G], (∀ g : G, IsOfFinOrder g) → ∀ i : G, orderOf i = 2 →
    (∀ g : G, Odd (orderOf (g⁻¹ * i * g * i))) → ∀ g : G, g * i * g⁻¹ * i⁻¹ ∈ oddCore G

Uses 1 · Used by 1

Statement usesOdd core from normal subgroups of odd-order elements

Used byA periodic counterexample to Borovik's question (Kourovka 11.13)

TheoremA periodic counterexample to Borovik's question (Kourovka 11.13)#●ready to prove

For a group \(G\), let \(O(G)\) be the join of all normal subgroups of \(G\) all of whose elements have odd order. There exist a periodic group \(G\) and an involution \(i \in G\) such that \(g^{-1} i g i\) has odd order for every \(g \in G\), but the image of \(i\) in \(G / O(G)\) is not central: \(g i g^{-1} i^{-1} \notin O(G)\) for some \(g \in G\). This answers Kourovka Problem 11.13 in the negative.

For finite groups the answer is yes, by Glauberman's \(Z^*\)-theorem.

public theorem_wanted periodicInvolutionCentralModOddCore_refuted :
    ¬ periodicInvolutionCentralModOddCore

Sources

• E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Archive of Solved Problems, Problem 11.13 (A. V. Borovik); resolution: E. B. Durakov and A. I. Sozutov, Algebra and Logic 52, no. 5 (2013), 422-425, Kourovka Archive, Problem 11.13: "No, not always", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesBorovik's question on involutions with odd-order products (Kourovka 11.13)

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.