Element orders of extensions of projective linear groups

AbbreviationProjective special linear group#✓fully proved

For a natural number \(n\) and a field \(F\), \(\mathrm{PSL}_n(F)\) is the quotient \(\mathrm{SL}_n(F)/Z(\mathrm{SL}_n(F))\) of the special linear group \(\mathrm{SL}_n(F)\) of \(n \times n\) matrices over \(F\) with determinant \(1\) by its centre.

abbrev PSL (n : ℕ) (F : Type) [Field F] : Type :=
  Matrix.SpecialLinearGroup (Fin n) F ⧸ Subgroup.center (Matrix.SpecialLinearGroup (Fin n) F)

Used by 1

Used byKourovka 14.60: new element orders in extensions of projective special linear groups

DefinitionKourovka 14.60: new element orders in extensions of projective special linear groups#✓fully proved

The proposition that for every \(n \ge 3\), every prime \(p\) and every \(k \ge 1\), with \(q = p^k\) and \(\mathbb{F}_q\) the field with \(q\) elements, the following holds: whenever \(H\) is a nontrivial normal subgroup of a finite group \(G\) and \(G/H\) is isomorphic to the projective special linear group \(\mathrm{PSL}_n(\mathbb{F}_q)\), some element of \(G\) has an order that is not the order of any element of \(G/H\).

def extensionOfPSLHasNewElementOrder : Prop :=
  ∀ (n p k : ℕ) [Fact p.Prime], 3 ≤ n → 0 < k →
    ∀ (G : Type) [Group G] [Finite G] (H : Subgroup G) [H.Normal], H ≠ ⊥ →
      Nonempty (G ⧸ H ≃* PSL n (GaloisField p k)) →
      ∃ g : G, ∀ y : G ⧸ H, orderOf y ≠ orderOf g

Uses 1 · Used by 1

Statement usesProjective special linear group

Used byExtensions of PSL have a new element order

TheoremExtensions of PSL have a new element order#●ready to prove

Resolved true: the Kourovka Archive answers 14.60 "Yes, it is true": Zavarnitsine proved it for n ≠ 4 and Grechkoseeva and Skresanov for n = 4 (the editors note that an earlier claim of failure for n = 4 was erroneous). Source: 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 14.60 (V. D. Mazurov); resolution: A. V. Zavarnitsine, Siberian Math. J. 49 (2008), 246-256 (n ≠ 4); M. A. Grechkoseeva and S. V. Skresanov, Siberian Electron. Math. Rep. 17 (2020), 585-589 (n = 4), Kourovka Archive, Problem 14.60 (answer: Yes, it is true; the editors note that an earlier claim of failure for n = 4 was erroneous).

public theorem_wanted extensionOfPSLHasNewElementOrder_holds : extensionOfPSLHasNewElementOrder

Uses 1

Statement usesKourovka 14.60: new element orders in extensions of projective special linear groups

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.