Dickson's classification of finite subgroups of PGL₂

AbbreviationAlgebraic closure of the field with p elements#✓fully proved

For a prime \(p\), \(K_p\) denotes a fixed algebraic closure of the finite field \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\).

noncomputable abbrev K : Type := AlgebraicClosure (ZMod p)
Used by 4
Used byDickson's classification, tame case · Dickson's classification, wild case · Projective general linear group of degree two · Projective special linear group of degree two

AbbreviationProjective general linear group of degree two#✓fully proved

For a prime \(p\), \(\mathrm{PGL}_2(K_p)\) is the quotient of the group \(\mathrm{GL}_2(K_p)\) of invertible \(2 \times 2\) matrices over the algebraic closure \(K_p\) of \(\mathbb{F}_p\) by its center.

abbrev PGL : Type := Matrix.ProjGenLinGroup (Fin 2) (K p)
Uses 1 · Used by 2
Statement usesAlgebraic closure of the field with p elements
Used byDickson's classification, tame case · Dickson's classification, wild case

AbbreviationProjective special linear group of degree two#✓fully proved

For a prime \(p\), \(\mathrm{PSL}_2(K_p)\) is the quotient of the group \(\mathrm{SL}_2(K_p)\) of \(2 \times 2\) matrices of determinant \(1\) over the algebraic closure \(K_p\) of \(\mathbb{F}_p\) by its center.

abbrev PSL : Type := Matrix.ProjectiveSpecialLinearGroup (Fin 2) (K p)
Uses 1
Statement usesAlgebraic closure of the field with p elements

TheoremDickson's classification, tame case#✓fully proved

Let \(p\) be an odd prime and let \(K\) be an algebraic closure of \(\mathbb{F}_p\). Every finite nontrivial subgroup \(G\) of \(\mathrm{PGL}_2(K)\) whose order is not divisible by \(p\) is cyclic, or isomorphic to the dihedral group of order \(2n\) for some \(n \ge 2\), or isomorphic to one of the groups \(A_4\), \(S_4\), \(A_5\).

Proof: Klein's orbit count on the projective line, followed by identification of the resulting orbit signatures.

theorem classification_tame (G : Subgroup (PGL p)) [Finite G]
    (hG_tame : ¬ (p : ℕ) ∣ Nat.card G)
    (hG_nontrivial : Nontrivial G) :
    (IsCyclic G) ∨
    (∃ n : ℕ, n ≥ 2 ∧ Nonempty (G ≃* DihedralGroup n)) ∨
    (Nonempty (G ≃* alternatingGroup (Fin 4))) ∨
    (Nonempty (G ≃* Equiv.Perm (Fin 4))) ∨
    (Nonempty (G ≃* alternatingGroup (Fin 5)))
Sources
  • L. E. Dickson, Linear Groups with an Exposition of the Galois Field Theory, Teubner (1901).
Uses 4
Statement usesAlgebraic closure of the field with p elements · Projective general linear group of degree two
Proof usesDihedral groups from a cyclic subgroup of index two · Burnside's lemma with a uniform fixed-point count

TheoremInjective ring maps induce injective maps of \(\mathrm{PGL}_n\)#✓fully proved

Let \(f : R \to S\) be an injective homomorphism of commutative rings and let \(n\) be a finite index set. Then the homomorphism \(\mathrm{PGL}_n(R) \to \mathrm{PGL}_n(S)\) induced by applying \(f\) to matrix entries is injective, where \(\mathrm{PGL}_n(R)\) denotes \(\mathrm{GL}_n(R)\) modulo its center.

theorem projGenLinGroup_map_injective {n R S : Type*} [Fintype n] [DecidableEq n]
    [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Injective f) :
    Function.Injective (Matrix.ProjGenLinGroup.map (n := n) f)
Used by 1
Used byDickson's classification, wild case

TheoremOrder of \(\mathrm{PGL}_2\) over a finite field#✓fully proved

If \(F\) is a finite field with \(q\) elements, then the projective general linear group \(\mathrm{PGL}_2(F)\) has order \(q(q^2 - 1)\).

theorem card_projGenLinGroup_fin_two (F : Type*) [Field F] [Fintype F] :
    Nat.card (Matrix.ProjGenLinGroup (Fin 2) F) =
      Fintype.card F * (Fintype.card F ^ 2 - 1)
Used by 1
Used byDickson's classification, wild case

TheoremOrder of \(\mathrm{PSL}_2\) over a finite field of odd characteristic#✓fully proved

Let \(F\) be a finite field with \(q\) elements whose characteristic \(p\) is not \(2\). Then the projective special linear group \(\mathrm{PSL}_2(F)\) has order \(q(q^2 - 1)/2\).

theorem card_projectiveSpecialLinearGroup_fin_two (p : ℕ) (F : Type*)
    [Field F] [Fintype F] [CharP F p] (hp2 : p ≠ 2) :
    Nat.card (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) =
      Fintype.card F * (Fintype.card F ^ 2 - 1) / 2
Used by 1
Used byDickson's classification, wild case

TheoremElements of \(\mathrm{PGL}_2\) of order divisible by the characteristic#✓fully proved

Let \(p\) be an odd prime and let \(F\) be a field of characteristic \(p\). If an element \(g\) of \(\mathrm{PGL}_2(F)\) has finite order and \(p\) divides the order of \(g\), then the order of \(g\) is \(p\).

theorem orderOf_eq_char_of_char_dvd
    {p : ℕ} [Fact (Nat.Prime p)] [Fact (2 < p)] {F : Type*} [Field F] [CharP F p]
    (g : Matrix.ProjGenLinGroup (Fin 2) F) (hfinite : orderOf g ≠ 0)
    (hdiv : p ∣ orderOf g) : orderOf g = p
Used by 1
Used byDickson's classification, wild case

TheoremDickson's classification, wild case#✓fully proved

Let \(p\) be an odd prime, let \(K\) be an algebraic closure of \(\mathbb{F}_p\), and let \(G\) be a finite subgroup of \(\mathrm{PGL}_2(K)\) whose order is divisible by \(p\). Then at least one of the following holds. (a) There are natural numbers \(m \ge 1\) and \(t\) with \(t\) coprime to \(p\) and \(t \mid p^m - 1\), and an injective homomorphism \(\varphi\) from the cyclic group \(\mathbb{Z}/t\mathbb{Z}\) to the automorphism group of the additive group \(\mathbb{F}_p^m\) such that \(\varphi(c)\) fixes no nonzero vector of \(\mathbb{F}_p^m\) for every \(c \ne 0\), and \(G\) is isomorphic to the semidirect product \(\mathbb{F}_p^m \rtimes_\varphi \mathbb{Z}/t\mathbb{Z}\). (b) \(G\) is isomorphic to \(\mathrm{PSL}_2(\mathbb{F}_{p^m})\) for some \(m \ge 1\), where \(\mathbb{F}_{p^m}\) is the field with \(p^m\) elements. (c) \(G\) is isomorphic to \(\mathrm{PGL}_2(\mathbb{F}_{p^m})\) for some \(m \ge 1\). (d) \(p = 3\) and \(G\) is isomorphic to the alternating group \(A_5\).

In the source, the first case is a group of maps \(z \mapsto az + b\) with \(a\) a root of unity; only the resulting abstract group structure is recorded here.

Proof: We follow X. Faber, Finite p-irregular subgroups of \(\mathrm{PGL}_2(k)\), arXiv:1112.1999, §6, using the Sylow normal form, exceptional-orbit count, and projective-line actions to identify the \(\mathrm{PSL}_2\), \(\mathrm{PGL}_2\), and \(A_5\) cases.

theorem classification_wild (G : Subgroup (PGL p)) [Finite G]
    (hG_p : p ∣ Nat.card G) :
    (∃ (m t : ℕ) (_ : m ≥ 1) (_ : Nat.Coprime t p) (_ : t ∣ p ^ m - 1)
      (φ : Multiplicative (ZMod t) →* MulAut (Multiplicative (Fin m → ZMod p)))
      (_hφ_injective : Function.Injective φ)
      (_hφ_fixed_point_free : ∀ c ≠ 1, ∀ v ≠ 1, φ c v ≠ v),
      Nonempty (G ≃* (Multiplicative (Fin m → ZMod p)) ⋊[φ] Multiplicative (ZMod t))) ∨
    (∃ m : ℕ, m ≥ 1 ∧
      Nonempty (G ≃* Matrix.ProjectiveSpecialLinearGroup (Fin 2) (GaloisField p m))) ∨
    (∃ m : ℕ, m ≥ 1 ∧
      Nonempty (G ≃* Matrix.ProjGenLinGroup (Fin 2) (GaloisField p m))) ∨
    (p = 3 ∧ Nonempty (G ≃* alternatingGroup (Fin 5)))
Sources
  • L. E. Dickson, Linear Groups with an Exposition of the Galois Field Theory, Teubner (1901).
Uses 6
Statement usesAlgebraic closure of the field with p elements · Projective general linear group of degree two
Proof usesOrder of \(\mathrm{PGL}_2\) over a finite field · Order of \(\mathrm{PSL}_2\) over a finite field of odd characteristic · Elements of \(\mathrm{PGL}_2\) of order divisible by the characteristic · Injective ring maps induce injective maps of \(\mathrm{PGL}_n\)
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.