Recognition of alternating groups by spectrum

DefinitionSpectrum of a group#✓fully proved

The spectrum \(\pi_e(G)\) of a group \(G\) is the set of orders of the elements of \(G\), where an element of infinite order is assigned order \(0\).

def elementOrders (G : Type*) [Group G] : Set ℕ :=
  Set.range (orderOf : G → ℕ)

Used by 1

Used byKourovka Problem 16.107 on recognition of alternating groups by spectrum

DefinitionKourovka Problem 16.107 on recognition of alternating groups by spectrum#✓fully proved

This proposition asserts that there is a natural number \(N\) such that for every \(n \ge N\), every finite group \(G\) with the same spectrum (set of element orders) as the alternating group \(A_n\) is isomorphic to \(A_n\).

def alternatingGroupRecognizableBySpectrum : Prop :=
  ∃ N : ℕ, ∀ n : ℕ, N ≤ n → ∀ (G : Type) [Group G] [Finite G],
    elementOrders G = elementOrders (alternatingGroup (Fin n)) →
      Nonempty (G ≃* alternatingGroup (Fin n))

Uses 1 · Used by 1

Statement usesSpectrum of a group

Used byLarge alternating groups are recognizable by spectrum

TheoremLarge alternating groups are recognizable by spectrum#●ready to prove

There is a natural number \(N\) such that for every \(n \ge N\), every finite group \(G\) whose set of element orders equals that of the alternating group \(A_n\) is isomorphic to \(A_n\).

public theorem_wanted alternatingGroupRecognizableBySpectrum_holds :
    alternatingGroupRecognizableBySpectrum

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 16.107 (W. J. Shi); resolution: I. B. Gorshkov, Recognizability of alternating groups by spectrum, Algebra and Logic 52 (2013), no. 1, 41-45, arXiv:1302.4825, abstract (the simple alternating groups Aₙ are recognizable by spectrum for n ≠ 6, 10); Kourovka Archive, Problem 16.107 (answer: Yes, it is), https://arxiv.org/abs/1302.4825.

Uses 1

Statement usesKourovka Problem 16.107 on recognition of alternating groups by spectrum

DefinitionSpectrum of a group#✓fully proved

The spectrum \(\omega(G)\) of a group \(G\) is the set of natural numbers that are orders of elements of \(G\), where an element of infinite order is assigned order \(0\).

def spectrum (G : Type*) [Group G] : Set ℕ :=
  Set.range (orderOf : G → ℕ)

Used by 1

Used byKourovka Problem 16.27 (statement)

DefinitionFinite composition series#✓fully proved

Let \(G\) be a group and \(m\) a natural number. A sequence \(s_0, s_1, \dots, s_m\) of subgroups of \(G\) is a composition series of length \(m\) if \(s_0\) is the trivial subgroup, \(s_m = G\), and for each \(i < m\) the subgroup \(s_i\) is a normal subgroup of \(s_{i+1}\) and the quotient \(s_{i+1}/s_i\) is a simple group.

def IsCompositionSeries {G : Type} [Group G] {m : ℕ} (s : Fin (m + 1) → Subgroup G) : Prop :=
  s 0 = ⊥ ∧ s (Fin.last m) = ⊤ ∧ ∀ i : Fin m, s i.castSucc ≤ s i.succ ∧
    ∃ _ : ((s i.castSucc).subgroupOf (s i.succ)).Normal,
      IsSimpleGroup (s i.succ ⧸ (s i.castSucc).subgroupOf (s i.succ))

Used by 1

Used byKourovka Problem 16.27 (statement)

DefinitionNon-abelian factor of a chain of subgroups#✓fully proved

Let \(G\) be a group, let \(s_0, s_1, \dots, s_m\) be subgroups of \(G\), and let \(i < m\). The \(i\)-th factor of the chain is non-abelian if \(s_i \cap s_{i+1}\) is a normal subgroup of \(s_{i+1}\) and the quotient group \(s_{i+1}/(s_i \cap s_{i+1})\) is non-abelian, that is, it has elements \(x, y\) with \(xy \ne yx\). When \(s_i \le s_{i+1}\), this quotient is \(s_{i+1}/s_i\).

def IsNonabelianFactor {G : Type} [Group G] {m : ℕ} (s : Fin (m + 1) → Subgroup G) (i : Fin m) :
    Prop :=
  ∃ _ : ((s i.castSucc).subgroupOf (s i.succ)).Normal,
    ∃ x y : s i.succ ⧸ (s i.castSucc).subgroupOf (s i.succ), x * y ≠ y * x

Used by 1

Used byKourovka Problem 16.27 (statement)

DefinitionKourovka Problem 16.27 (statement)#✓fully proved

The statement that for every natural number \(n\) and every finite group \(G\) whose spectrum, the set of orders of its elements, equals the spectrum of the alternating group \(A_n\), every composition series of \(G\) has at most one non-abelian factor.

The problem was posed by A. V. Vasil'ev and V. D. Mazurov.

def alternatingSpectrumOneNonabelianFactor : Prop :=
  ∀ (n : ℕ) (G : Type) [Group G] [Finite G], spectrum G = spectrum (alternatingGroup (Fin n)) →
    ∀ (m : ℕ) (s : Fin (m + 1) → Subgroup G), IsCompositionSeries s →
      ∀ i j : Fin m, IsNonabelianFactor s i → IsNonabelianFactor s j → i = j

Uses 3 · Used by 1

Statement usesFinite composition series · Non-abelian factor of a chain of subgroups · Spectrum of a group

Used byGroups isospectral to an alternating group (Kourovka Problem 16.27)

TheoremGroups isospectral to an alternating group (Kourovka Problem 16.27)#●ready to prove

Let \(n\) be a natural number and let \(G\) be a finite group whose spectrum, the set of orders of its elements, equals the spectrum of the alternating group \(A_n\). Then every composition series of \(G\) has at most one non-abelian factor.

public theorem_wanted alternatingSpectrumOneNonabelianFactor_holds :
    alternatingSpectrumOneNonabelianFactor

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 16.27 (A. V. Vasil'ev and V. D. Mazurov); resolution: I. B. Gorshkov, Algebra and Logic 52 (2013), no. 1, 41-45, Kourovka Archive, Problem 16.27 (Yes, it is).

Uses 1

Statement usesKourovka Problem 16.27 (statement)

DefinitionKourovka Problem 19.80 (\(OC_7\)-groups)#✓fully proved

The proposition, asked by W. J. Shi, that every \(OC_7\)-group, that is, every group whose set of element orders is exactly \(\{1, 2, \dots, 7\}\) (such a group is periodic), is isomorphic to the alternating group \(A_7\).

def ocSevenGroupIsAlternating : Prop :=
  ∀ (G : Type) [Group G], Set.range (fun g : G => orderOf g) = Set.Icc 1 7 →
    Nonempty (G ≃* alternatingGroup (Fin 7))

Used by 1

Used byGroups with element orders \(1\) to \(7\) are isomorphic to \(A_7\)

TheoremGroups with element orders \(1\) to \(7\) are isomorphic to \(A_7\)#●ready to prove

Every group, finite or infinite, whose set of element orders is exactly \(\{1, 2, \dots, 7\}\) is isomorphic to the alternating group \(A_7\). This answers Kourovka Problem 19.80 positively (Mamontov and Jabara).

public theorem_wanted ocSevenGroupIsAlternating_holds : ocSevenGroupIsAlternating

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 19.80 (W. J. Shi); resolution: A. S. Mamontov and E. Jabara, Recognizing A₇ by its set of element orders, Siberian Math. J. 62 (2021), no. 1, 93-104, doi:10.1134/S0037446621010109, Kourovka Archive, Problem 19.80: Yes, it is true, https://arxiv.org/abs/1401.0300v49.

Uses 1

Statement usesKourovka Problem 19.80 (\(OC_7\)-groups)

7 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.