Periodic groups with {3, 5}-involutions

DefinitionInvolution#✓fully proved

An element \(x\) of a group \(G\) is an involution when \(x^2 = 1\) and \(x \ne 1\).

def IsInvolution {G : Type*} [Group G] (x : G) : Prop :=
  x ^ 2 = 1 ∧ x ≠ 1

Used by 1

Used byJabara's conjecture on groups with \(\{3, 5\}\)-involutions

DefinitionThe special unitary group \(\mathrm{SU}_3(4)\)#✓fully proved

Let \(\mathbb{F}_{16}\) be the field with \(16\) elements and, for a matrix \(A\) over \(\mathbb{F}_{16}\), let \(\bar{A}\) be the matrix obtained by applying the involutive field automorphism \(x \mapsto x^4\) of \(\mathbb{F}_{16}\) to each entry. Then \(\mathrm{SU}_3(4)\) is the subgroup of \(\mathrm{GL}_3(\mathbb{F}_{16})\) generated by the invertible \(3 \times 3\) matrices \(A\) over \(\mathbb{F}_{16}\) with \(\det A = 1\) and \(\bar{A}^{\top} A = 1\), that is, by the determinant-one isometries of the Hermitian form \(x_1 \bar{y}_1 + x_2 \bar{y}_2 + x_3 \bar{y}_3\).

These matrices already form a subgroup, so \(\mathrm{SU}_3(4)\) consists exactly of them.

noncomputable def specialUnitaryGroupThreeFour : Subgroup (GL (Fin 3) (GaloisField 2 4)) :=
  Subgroup.closure {A | Matrix.transpose ((A : Matrix (Fin 3) (Fin 3) (GaloisField 2 4)).map
      (· ^ 4)) * (A : Matrix (Fin 3) (Fin 3) (GaloisField 2 4)) = 1 ∧
    (A : Matrix (Fin 3) (Fin 3) (GaloisField 2 4)).det = 1}

Used by 2

Used byThe projective special unitary group \(\mathrm{PSU}_3(4)\) · Jabara's conjecture on groups with \(\{3, 5\}\)-involutions

AbbreviationThe projective special unitary group \(\mathrm{PSU}_3(4)\)#✓fully proved

It is the quotient \(\mathrm{PSU}_3(4) = \mathrm{SU}_3(4) / Z(\mathrm{SU}_3(4))\) of the special unitary group \(\mathrm{SU}_3(4)\) by its centre \(Z(\mathrm{SU}_3(4))\).

abbrev PSUThreeFour :=
  specialUnitaryGroupThreeFour ⧸ Subgroup.center specialUnitaryGroupThreeFour

Uses 1 · Used by 1

Statement usesThe special unitary group \(\mathrm{SU}_3(4)\)

Used byJabara's conjecture on groups with \(\{3, 5\}\)-involutions

DefinitionJabara's conjecture on groups with \(\{3, 5\}\)-involutions#✓fully proved

Kourovka 19.36 (E. Jabara): let \(G\) be a periodic group (every element has finite order) that is generated by its involutions (elements \(x \ne 1\) with \(x^2 = 1\)). Suppose that the order of \(xy\) lies in \(\{1, 2, 3, 5\}\) for all involutions \(x, y\) of \(G\), and that each of these four values is the order of \(xy\) for some involutions \(x, y\) of \(G\). Then \(G\) is isomorphic to the alternating group \(A_5\) or to the projective special unitary group \(\mathrm{PSU}_3(4)\).

def threeFiveInvolutionsClassification : Prop :=
  ∀ (G : Type) [Group G], IsMulTorsion G →
    Subgroup.closure {x : G | IsInvolution x} = ⊤ →
    (∀ x y : G, IsInvolution x → IsInvolution y → orderOf (x * y) ∈ ({1, 2, 3, 5} : Set ℕ)) →
    (∀ d ∈ ({1, 2, 3, 5} : Set ℕ), ∃ x y : G, IsInvolution x ∧ IsInvolution y ∧
      orderOf (x * y) = d) →
    Nonempty (G ≃* alternatingGroup (Fin 5)) ∨ Nonempty (G ≃* PSUThreeFour)

Uses 3 · Used by 1

Statement usesInvolution · The projective special unitary group \(\mathrm{PSU}_3(4)\) · The special unitary group \(\mathrm{SU}_3(4)\)

Used byJabara's conjecture on groups with \(\{3, 5\}\)-involutions holds

TheoremJabara's conjecture on groups with \(\{3, 5\}\)-involutions holds#●ready to prove

Let \(G\) be a periodic group (every element has finite order) that is generated by its involutions (elements \(x \ne 1\) with \(x^2 = 1\)). Suppose that the order of \(xy\) lies in \(\{1, 2, 3, 5\}\) for all involutions \(x, y\) of \(G\), and that each of these four values is the order of \(xy\) for some involutions \(x, y\) of \(G\). Then \(G\) is isomorphic to the alternating group \(A_5\) or to the projective special unitary group \(\mathrm{PSU}_3(4)\).

Bettio proved this even without the hypothesis that \(G\) is periodic; the Kourovka Archive records the proof.

public theorem_wanted threeFiveInvolutionsClassification_holds : threeFiveInvolutionsClassification

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.36 (E. Jabara); resolution: E. Bettio, A proof of a conjecture by Jabara on groups in which all involutions are odd transpositions, J. Group Theory 24 (2021), no. 5, 1055-1067, abstract: a group generated by elements of order two in which the product of any two such elements has order 1, 2, 3 or 5, with all possibilities occurring, is isomorphic to A₅ or to PSU(3, 4), answering Problem 19.36; Kourovka Archive, Problem 19.36: the conjecture is proved, even without using the hypothesis that G is periodic, https://doi.org/10.1515/jgth-2020-0129.

Uses 1

Statement usesJabara's conjecture on groups with \(\{3, 5\}\)-involutions

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.