Products of large normal subsets
DefinitionLarge inverse-closed normal subsets with small square#✓fully proved
A group \(G\) has this property when it has a subset \(S\) such that \(g s g^{-1} \in S\) and \(s^{-1} \in S\) for all \(g \in G\) and \(s \in S\), \(S\) has more than \(|G| / \log_2 |G|\) elements, and \(S^2 = \{st : s, t \in S\}\) is not all of \(G\).
The definition is intended for finite groups \(G\).
DefinitionPyber's conjecture for finite simple groups (Kourovka 20.74(a))#✓fully proved
This proposition states that there is a natural number \(N\) such that every nonabelian finite simple group \(G\) that has a subset \(S\) closed under conjugation and under inversion with \(|S| > |G| / \log_2 |G|\) and \(S^2 \ne G\), where \(S^2 = \{st : s, t \in S\}\), has order \(|G| \le N\). Since there are only finitely many groups of each order, this says that only finitely many such groups exist up to isomorphism.
def finitelyManySimpleGroupsWithLargeNormalSubset : Prop :=
∃ N : ℕ, ∀ (G : Type) [Group G] [Finite G], IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
HasLargeInverseClosedNormalSubsetWithSmallSquare G → Nat.card G ≤ N
def HasLargeInverseClosedNormalSubsetWithSmallSquare (G : Type) [Group G] : Prop :=
∃ S : Set G, (∀ g s : G, s ∈ S → g * s * g⁻¹ ∈ S) ∧ (∀ s ∈ S, s⁻¹ ∈ S) ∧
(Nat.card G : ℝ) / Real.logb 2 (Nat.card G) < S.ncard ∧ S * S ≠ Set.univ
WantedExt/GroupTheory/LargeNormalSubsetSquareKourovka20Problem74Wanted.lean:43
Uses 1 · Used by 1
DefinitionPyber's conjecture for \(\mathrm{PSL}(2, p)\) (Kourovka 20.74(b))#✓fully proved
This proposition states that there is a natural number \(N\) such that \(p \le N\) for every prime \(p\) for which the group \(G = \mathrm{PSL}(2, p)\), the quotient of \(\mathrm{SL}(2, \mathbb{Z}/p\mathbb{Z})\) by its center, has a subset \(S\) closed under conjugation and under inversion with \(|S| > |G| / \log_2 |G|\) and \(S^2 \ne G\), where \(S^2 = \{st : s, t \in S\}\). In other words, only finitely many groups \(\mathrm{PSL}(2, p)\) with \(p\) prime have such a subset.
def finitelyManyPSL2WithLargeNormalSubset : Prop :=
∃ N : ℕ, ∀ p : ℕ, p.Prime →
HasLargeInverseClosedNormalSubsetWithSmallSquare
(Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod p)) → p ≤ N
def HasLargeInverseClosedNormalSubsetWithSmallSquare (G : Type) [Group G] : Prop :=
∃ S : Set G, (∀ g s : G, s ∈ S → g * s * g⁻¹ ∈ S) ∧ (∀ s ∈ S, s⁻¹ ∈ S) ∧
(Nat.card G : ℝ) / Real.logb 2 (Nat.card G) < S.ncard ∧ S * S ≠ Set.univ
WantedExt/GroupTheory/LargeNormalSubsetSquareKourovka20Problem74Wanted.lean:43
Uses 1 · Used by 1
TheoremPyber's conjecture for finite simple groups is false#●ready to prove
There is no natural number \(N\) such that every nonabelian finite simple group \(G\) that has a subset \(S\) with \(g s g^{-1} \in S\) and \(s^{-1} \in S\) for all \(g \in G\) and \(s \in S\), with \(|S| > |G| / \log_2 |G|\) and with \(S^2 \ne G\), where \(S^2 = \{st : s, t \in S\}\), has order \(|G| \le N\).
Sheinfeld (Theorem 1.6) gives, for every odd \(n \ge 5\), an inverse-closed normal subset \(S\) of the simple group \(G = \mathrm{PSL}_n(5) = \mathrm{SL}_n(5)\) with \(|S| \ge |G| / 960\) and \(S^2 \ne G\), so infinitely many nonabelian finite simple groups have such a subset; the paper states that this disproves Pyber's conjecture, and the 21st issue of the Kourovka Notebook records 20.74(a) as "No, there are infinitely many such groups".
public theorem_wanted finitelyManySimpleGroupsWithLargeNormalSubset_refuted :
¬ finitelyManySimpleGroupsWithLargeNormalSubset
def finitelyManySimpleGroupsWithLargeNormalSubset : Prop :=
∃ N : ℕ, ∀ (G : Type) [Group G] [Finite G], IsSimpleGroup G → (∃ a b : G, a * b ≠ b * a) →
HasLargeInverseClosedNormalSubsetWithSmallSquare G → Nat.card G ≤ N
WantedExt/GroupTheory/LargeNormalSubsetSquareKourovka20Problem74Wanted.lean:49
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.74 (L. Pyber); resolution: O. Sheinfeld, On Shalev's quantitative version of Thompson's conjecture, preprint, arXiv:2609.22004 (2026) (part (a)); S. V. Skresanov, Bull. London Math. Soc. 57 (2025), no. 11, 3429-3440 (part (b)), (a) Sheinfeld, Theorem 1.6: for every odd n ≥ 5 there is an inverse-closed normal subset S ⊆ SL_n(5) = PSL_n(5) with |S| ≥ |SL_n(5)|/960 and diag(1, -I_{n-1}) ∉ S², which the paper states disproves Pyber's conjecture; (b) Skresanov, Corollary 3 (arXiv:2406.12506): in a finite simple group of Lie type of bounded rank every inverse-closed normal subset A with |A| > |G|/log₂|G| has A² = G once |G| is large in terms of the rank, and part (b) for PSL(2, p) follows; Kourovka Notebook (21st issue), Problem 20.74: a) No, there are infinitely many such groups; b) The conjecture is proved for the groups PSL(2, p), https://arxiv.org/abs/2609.22004.
Uses 1
TheoremPyber's conjecture for \(\mathrm{PSL}(2, p)\) holds#●ready to prove
There is a natural number \(N\) such that for every prime \(p\) the following holds. Let \(G = \mathrm{PSL}(2, p)\) be the quotient of \(\mathrm{SL}(2, \mathbb{Z}/p\mathbb{Z})\) by its center. If \(G\) has a subset \(S\) with \(g s g^{-1} \in S\) and \(s^{-1} \in S\) for all \(g \in G\) and \(s \in S\), with more than \(|G| / \log_2 |G|\) elements, and with \(S^2 = \{st : s, t \in S\}\) different from \(G\), then \(p \le N\). In other words, only finitely many groups \(\mathrm{PSL}(2, p)\) with \(p\) prime have such a subset.
Skresanov (Bull. London Math. Soc. 57 (2025), Corollary 3) proves that in a finite simple group \(G\) of Lie type of bounded rank every inverse-closed normal subset \(A\) with \(|A| > |G| / \log_2 |G|\) satisfies \(A^2 = G\) once \(|G|\) is large, and notes that this settles the groups \(\mathrm{PSL}(2, p)\); the 21st issue of the Kourovka Notebook records 20.74(b) as proved for the groups \(\mathrm{PSL}(2, p)\).
public theorem_wanted finitelyManyPSL2WithLargeNormalSubset_holds :
finitelyManyPSL2WithLargeNormalSubset
def finitelyManyPSL2WithLargeNormalSubset : Prop :=
∃ N : ℕ, ∀ p : ℕ, p.Prime →
HasLargeInverseClosedNormalSubsetWithSmallSquare
(Matrix.ProjectiveSpecialLinearGroup (Fin 2) (ZMod p)) → p ≤ N
WantedExt/GroupTheory/LargeNormalSubsetSquareKourovka20Problem74Wanted.lean:55
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.74 (L. Pyber); resolution: O. Sheinfeld, On Shalev's quantitative version of Thompson's conjecture, preprint, arXiv:2609.22004 (2026) (part (a)); S. V. Skresanov, Bull. London Math. Soc. 57 (2025), no. 11, 3429-3440 (part (b)), (a) Sheinfeld, Theorem 1.6: for every odd n ≥ 5 there is an inverse-closed normal subset S ⊆ SL_n(5) = PSL_n(5) with |S| ≥ |SL_n(5)|/960 and diag(1, -I_{n-1}) ∉ S², which the paper states disproves Pyber's conjecture; (b) Skresanov, Corollary 3 (arXiv:2406.12506): in a finite simple group of Lie type of bounded rank every inverse-closed normal subset A with |A| > |G|/log₂|G| has A² = G once |G| is large in terms of the rank, and part (b) for PSL(2, p) follows; Kourovka Notebook (21st issue), Problem 20.74: a) No, there are infinitely many such groups; b) The conjecture is proved for the groups PSL(2, p), https://arxiv.org/abs/2609.22004.
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.