p-parts of conjugacy class sizes

DefinitionGroups with a normal p-complement#✓fully proved

A group \(G\) has a normal \(p\)-complement when it has a normal subgroup \(N\) and a Sylow \(p\)-subgroup \(P\) that are complements of each other: every element of \(G\) can be written uniquely as \(nq\) with \(n \in N\) and \(q \in P\).

def HasNormalPComplement (p : ℕ) (G : Type*) [Group G] : Prop :=
  ∃ (N : Subgroup G) (P : Sylow p G), N.Normal ∧ N.IsComplement' P

Used by 1

Used byGorshkov's problem on maximal p-parts of class sizes

DefinitionGorshkov's problem on maximal p-parts of class sizes#✓fully proved

For a prime \(p\), the \(p\)-part of a positive integer \(m\) is the largest power of \(p\) dividing \(m\). This is the statement that for every finite group \(G\), every prime \(p\) and every \(p\)-element \(g\) of \(G\) (that is, \(g^{p^k} = 1\) for some natural number \(k\)), if for every \(x \in G\) the \(p\)-part of the size of the conjugacy class of \(x\) is at most the \(p\)-part of the size of the conjugacy class of \(g\), then \(G\) has a normal \(p\)-complement.

This is Kourovka Notebook Problem 20.27 (I. B. Gorshkov).

def maximalClassSizePElementGivesNormalComplement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] (p : ℕ), p.Prime → ∀ g : G, (∃ k : ℕ, g ^ p ^ k = 1) →
    (∀ x : G, ordProj[p] (Nat.card (ConjClasses.mk x).carrier) ≤
      ordProj[p] (Nat.card (ConjClasses.mk g).carrier)) →
    HasNormalPComplement p G

def HasNormalPComplement (p : ℕ) (G : Type*) [Group G] : Prop :=
  ∃ (N : Subgroup G) (P : Sylow p G), N.Normal ∧ N.IsComplement' P

WantedExt/GroupTheory/MaximalClassSizePElementNormalComplementKourovka20Problem27Wanted.lean:42

Uses 1 · Used by 1

Statement usesGroups with a normal p-complement

Used byA maximal p-part of a class size does not force a normal p-complement

TheoremA maximal p-part of a class size does not force a normal p-complement#●ready to prove

For a prime \(p\), the \(p\)-part of a positive integer \(m\) is the largest power of \(p\) dividing \(m\). There exist a finite group \(G\), a prime \(p\) and a \(p\)-element \(g\) of \(G\) (that is, \(g^{p^k} = 1\) for some natural number \(k\)) such that for every \(x \in G\) the \(p\)-part of the size of the conjugacy class of \(x\) is at most the \(p\)-part of the size of the conjugacy class of \(g\), but \(G\) has no normal \(p\)-complement.

Sambale's counterexample is the group \(\mathrm{SL}(2, 3) \rtimes Q_8\) of order \(192\) (number \(945\) in the GAP library of small groups) with \(p = 2\). In it an element of order \(4\) has class size \(24\), whose \(2\)-part \(8\) is the largest \(2\)-part of a class size, while the eight elements of order \(3\) form one conjugacy class, so there is no normal subgroup of order \(3\), that is, no normal \(2\)-complement.

public theorem_wanted maximalClassSizePElementGivesNormalComplement_refuted :
    ¬ maximalClassSizePElementGivesNormalComplement

def maximalClassSizePElementGivesNormalComplement : Prop :=
  ∀ (G : Type) [Group G] [Finite G] (p : ℕ), p.Prime → ∀ g : G, (∃ k : ℕ, g ^ p ^ k = 1) →
    (∀ x : G, ordProj[p] (Nat.card (ConjClasses.mk x).carrier) ≤
      ordProj[p] (Nat.card (ConjClasses.mk g).carrier)) →
    HasNormalPComplement p G

WantedExt/GroupTheory/MaximalClassSizePElementNormalComplementKourovka20Problem27Wanted.lean:47

Sources

E. I. Khukhro and V. D. Mazurov (eds.), Unsolved Problems in Group Theory: The Kourovka Notebook, 21st issue, arXiv:1401.0300v49 (2026), Problem 20.27 (I. B. Gorshkov); resolution: B. Sambale, letter of 16 February 2022, recorded in the Kourovka Notebook (21st issue), Problem 20.27: "No, not necessarily, a counterexample is given by SmallGroup(192,945)", https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesGorshkov's problem on maximal p-parts of class sizes

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.