Linear groups

Groups of matrices over fields and rings: SL2, PGL2 and SU(2) and their conjugacy and subgroups (Dickson's classification), Jordan, Malcev and Selberg theorems, transvections, eigenvalues of elements of prime order, and linearity of specific groups.

TheoremExponent of the general linear group over a prime field#✓fully proved

Let \(p\) be a prime and let \(m \ge 1\). The exponent of the group \(\mathrm{GL}_m(\mathbb{F}_p)\) of invertible \(m \times m\) matrices over \(\mathbb{F}_p = \mathbb{Z}/p\mathbb{Z}\) is

\[p^{\lceil \log_p m \rceil} \cdot \operatorname{lcm}(p - 1, p^2 - 1, \dots, p^m - 1),\]

and this number equals \(p^{\lceil \log_p m \rceil} \prod_{k=1}^{m} \Phi_k(p)\), where \(\Phi_k\) denotes the \(k\)-th cyclotomic polynomial.

theorem generalLinearGroup_exponent_eq_lcm_eq_cyclotomicProduct
    (p m : ℕ) (hp : p.Prime) (hm : 0 < m) :
    Monoid.exponent (Matrix.GeneralLinearGroup (Fin m) (ZMod p)) =
        p ^ Nat.clog p m * (Finset.range m).lcm (fun i => p ^ (i + 1) - 1) ∧
      ((p ^ Nat.clog p m * (Finset.range m).lcm (fun i => p ^ (i + 1) - 1) : ℕ) : ℤ) =
        (p : ℤ) ^ Nat.clog p m *
          ∏ k ∈ Finset.Icc 1 m, (Polynomial.cyclotomic k ℤ).eval (p : ℤ)
Sources
  • Eugene Karolinsky and Dmytro Seliutin, Carmichael Numbers for GL(m), Journal of Integer Sequences 23 (2020), Article 20.10.6, https://cs.uwaterloo.ca/journals/JIS/VOL23/Karolinsky/kar2.tex, Theorem fermat_matr (quoting J. B. Marshall, On the extension of Fermat's theorem to matrices of order n, Proc. Edinb. Math. Soc. 6 (1939), and I. Niven, Fermat's theorem for matrices, Duke Math. J. 15 (1948)), lines 139-144; the lcm/cyclotomic identity is the paper's Proposition, lines 113-118.

TheoremJordan's theorem on finite linear groups#✓fully proved

For every natural number \(n\) there is a natural number \(J\) such that every finite subgroup \(G\) of \(\mathrm{GL}_n(\mathbb{C})\) contains an abelian subgroup \(A\) that is normal in \(G\) and has index \([G : A] \le J\).

public theorem jordan_linear_groups
    (n : ℕ) : ∃ J : ℕ, ∀ (G : Subgroup (Matrix.GeneralLinearGroup (Fin n) Complex)),
      Finite ↥G →
        ∃ (A : Subgroup (Matrix.GeneralLinearGroup (Fin n) Complex)),
          A ≤ G ∧
          (∀ g ∈ G, ∀ a ∈ A, g * a * g⁻¹ ∈ A) ∧
          (∀ x ∈ A, ∀ y ∈ A, x * y = y * x) ∧
          A.relIndex G ≤ J
Sources
  • C. Jordan, J. Reine Angew. Math. 84 (1878); Lean states complex GL_n specialization GL_n(ℂ) while general theorem holds over any char-zero field with bound depending only on n.

TheoremMalcev's theorem on linear groups#✓fully proved

Let \(K\) be a field and \(n\) a natural number. Every finitely generated subgroup of the general linear group \(\mathrm{GL}_n(K)\) is residually finite.

theorem malcev_residuallyFinite
    {K : Type*} [Field K] {n : ℕ}
    (G : Subgroup (Matrix.GeneralLinearGroup (Fin n) K))
    (hFG : Group.FG G) : Group.ResiduallyFinite G
Sources
  • A. I. Malcev, Mat. Sb. 8 (1940) 405–422; Wehrfritz, Infinite Linear Groups; Lean states subgroup G ≤ GL_n(K) with Group.FG G.

TheoremSelberg's lemma#✓fully proved

Let \(K\) be a field of characteristic zero and let \(n\) be a natural number. Every finitely generated subgroup \(G\) of \(\mathrm{GL}_n(K)\) has a subgroup \(H\) of finite index in \(G\) that is torsion-free: the identity is the only element of finite order in \(H\).

theorem selberg_finiteIndex_torsionFree
    {K : Type*} [Field K] [CharZero K] {n : ℕ}
    (G : Subgroup (Matrix.GeneralLinearGroup (Fin n) K))
    (hFG : Group.FG G) :
    ∃ H : Subgroup G, H.FiniteIndex ∧ IsMulTorsionFree H
Sources
  • A. Selberg, Contributions to Function Theory (1960) Selberg's lemma; Alperin, Proc. AMS 1969; Lean states char-zero case with H not required normal.

DefinitionStable sets of linear automorphisms#✓fully proved

Let \(V\) be a vector space over a field \(K\). A set \(S\) of \(K\)-linear automorphisms of \(V\) is stable when there are a natural number \(m\) and subspaces \(0 = W_0 \le W_1 \le \cdots \le W_m = V\) of \(V\) such that \(g(w) - w \in W_i\) for every \(i < m\), every \(g \in S\) and every \(w \in W_{i+1}\).

def HasStableSeries {K V : Type} [Field K] [AddCommGroup V] [Module K V]
    (S : Set (V ≃ₗ[K] V)) : Prop :=
  ∃ (m : ℕ) (W : Fin (m + 1) → Submodule K V), W 0 = ⊥ ∧ W (Fin.last m) = ⊤ ∧
    (∀ i : Fin m, W i.castSucc ≤ W i.succ) ∧
    ∀ i : Fin m, ∀ g ∈ S, ∀ w ∈ W i.succ, g w - w ∈ W i.castSucc
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.