Abelian subgroups of p-groups

DefinitionPyber's question on generators of abelian subgroups (Kourovka 20.75)#✓fully proved

The proposition that for every prime \(p\), every natural number \(k\) and every finite \(p\)-group \(G\), if every abelian normal subgroup of \(G\) can be generated by at most \(k\) elements, then every abelian subgroup of \(G\) can be generated by at most \(2k\) elements.

def abelianSubgroupGeneratorsLeTwiceNormal : Prop :=
  ∀ (p k : ℕ) (G : Type) [Group G] [Finite G], p.Prime → IsPGroup p G →
    (∀ A : Subgroup G, A.Normal → (∀ x ∈ A, ∀ y ∈ A, x * y = y * x) →
      ∃ s : Finset G, s.card ≤ k ∧ Subgroup.closure (s : Set G) = A) →
    ∀ B : Subgroup G, (∀ x ∈ B, ∀ y ∈ B, x * y = y * x) →
      ∃ s : Finset G, s.card ≤ 2 * k ∧ Subgroup.closure (s : Set G) = B

Used by 1

Used byKourovka Problem 20.75 has a negative answer

TheoremKourovka Problem 20.75 has a negative answer#●ready to prove

The statement of Kourovka Problem 20.75 is false: there are a prime \(p\), a natural number \(k\), a finite \(p\)-group \(G\) all of whose abelian normal subgroups can be generated by at most \(k\) elements, and an abelian subgroup of \(G\) that cannot be generated by at most \(2k\) elements.

Muliarchyk's counterexample (Theorem 1.1) is a finite \(2\)-group of order \(2^{110N+1}\), with \(N = 2124210350\), whose abelian normal subgroups can be generated by \(32N + 1\) elements while an elementary abelian subgroup needs \(65N > 2(32N + 1)\) generators; the 21st issue of the Kourovka Notebook marks 20.75 solved ("No, it is not").

public theorem_wanted abelianSubgroupGeneratorsLeTwiceNormal_refuted :
    ¬ abelianSubgroupGeneratorsLeTwiceNormal

def abelianSubgroupGeneratorsLeTwiceNormal : Prop :=
  ∀ (p k : ℕ) (G : Type) [Group G] [Finite G], p.Prime → IsPGroup p G →
    (∀ A : Subgroup G, A.Normal → (∀ x ∈ A, ∀ y ∈ A, x * y = y * x) →
      ∃ s : Finset G, s.card ≤ k ∧ Subgroup.closure (s : Set G) = A) →
    ∀ B : Subgroup G, (∀ x ∈ B, ∀ y ∈ B, x * y = y * x) →
      ∃ s : Finset G, s.card ≤ 2 * k ∧ Subgroup.closure (s : Set G) = B

WantedExt/GroupTheory/AbelianNormalGeneratorsPGroupKourovka20Problem75Wanted.lean:38

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.75 (L. Pyber); resolution: K. Muliarchyk, An explicit counterexample to Kourovka Notebook Problem 20.75, preprint (2026), Kourovka Notebook site, Theorem 1.1: for N = 2124210350 an explicitly specified finite 2-group of order 2^(110N+1) in which every abelian normal subgroup can be generated by at most 32N + 1 elements and some elementary abelian subgroup needs 65N generators; Kourovka Notebook (21st issue), Problem 20.75: No, it is not, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/kourovka_20.75_solution.pdf.

Uses 1

Statement usesPyber's question on generators of abelian subgroups (Kourovka 20.75)

DefinitionPyber's question on orders of abelian subgroups (Kourovka 20.76)#✓fully proved

The proposition that for every prime \(p\), every natural number \(k\) and every finite \(p\)-group \(G\), if every abelian normal subgroup of \(G\) has order at most \(p^k\), then every abelian subgroup of \(G\) has order at most \(p^{2k}\).

def abelianSubgroupOrderLeSquareNormal : Prop :=
  ∀ (p k : ℕ) (G : Type) [Group G] [Finite G], p.Prime → IsPGroup p G →
    (∀ A : Subgroup G, A.Normal → (∀ x ∈ A, ∀ y ∈ A, x * y = y * x) → Nat.card A ≤ p ^ k) →
    ∀ B : Subgroup G, (∀ x ∈ B, ∀ y ∈ B, x * y = y * x) → Nat.card B ≤ p ^ (2 * k)

Used by 1

Used byKourovka Problem 20.76 has a negative answer

TheoremKourovka Problem 20.76 has a negative answer#●ready to prove

The statement of Kourovka Problem 20.76 is false: there are a prime \(p\), a natural number \(k\), a finite \(p\)-group \(G\) all of whose abelian normal subgroups have order at most \(p^k\), and an abelian subgroup of \(G\) of order greater than \(p^{2k}\).

Muliarchyk's counterexample (Theorem 1.1) is a finite \(2\)-group of order \(2^{144e+1}\), with \(e = 256363762\), whose abelian normal subgroups have order at most \(2^{42e}\) while it has an elementary abelian subgroup of order \(2^{85e} > 2^{84e}\); the 21st issue of the Kourovka Notebook marks 20.76 solved ("No, it is not").

public theorem_wanted abelianSubgroupOrderLeSquareNormal_refuted :
    ¬ abelianSubgroupOrderLeSquareNormal

def abelianSubgroupOrderLeSquareNormal : Prop :=
  ∀ (p k : ℕ) (G : Type) [Group G] [Finite G], p.Prime → IsPGroup p G →
    (∀ A : Subgroup G, A.Normal → (∀ x ∈ A, ∀ y ∈ A, x * y = y * x) → Nat.card A ≤ p ^ k) →
    ∀ B : Subgroup G, (∀ x ∈ B, ∀ y ∈ B, x * y = y * x) → Nat.card B ≤ p ^ (2 * k)

WantedExt/GroupTheory/AbelianNormalOrderPGroupKourovka20Problem76Wanted.lean:37

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.76 (L. Pyber); resolution: K. Muliarchyk, Abelian subgroups of finite 2-groups: counterexamples to Problems 20.75 and 20.76, preprint (2026), Kourovka Notebook site, Theorem 1.1: for e = 256363762 an explicitly specified finite 2-group of order 2^(144e+1) whose abelian normal subgroups have order at most 2^(42e), with an elementary abelian subgroup of order 2^(85e) (p = 2, k = 42e); Kourovka Notebook (21st issue), Problem 20.76: No, it is not, https://kourovkanotebookorg.wordpress.com/wp-content/uploads/2026/09/kourovka_20_75-20_76_solution.pdf.

Uses 1

Statement usesPyber's question on orders of abelian subgroups (Kourovka 20.76)

2 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.