Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_GL2ConjugacyCells.lean

definition module

Conjugacy-type predicates and cells in

Over a field K, four predicates on a 2\times 2 matrix M with entries in K are defined, each phrased in terms of the matrix itself or its characteristic polynomial M.charpoly. IsCentralType M asserts that M = c\cdot 1 for some scalar c \in K, i.e. M is a scalar multiple of the identity. IsUnipotentType M is the conjunction of two conditions: M is not of central type, and there exists a \in K with M.\mathrm{charpoly} = (X - a)^2; thus the characteristic polynomial has a single repeated rational eigenvalue while M itself is non-scalar, which covers the unipotent matrices and their scalar twists. IsHyperbolicType M asserts the existence of a, b \in K with a \neq b and M.\mathrm{charpoly} = (X-a)(X-b), i.e. two distinct eigenvalues in K. IsEllipticType M asserts that no a \in K is a root of M.\mathrm{charpoly}, i.e. the characteristic polynomial is irreducible over K (for a degree-two polynomial, having no rational root).

Correspondingly four subsets of the general linear group \mathrm{GL}_2(K) are defined — centralCell, unipotentCell, hyperbolicCell and ellipticCell — each consisting of those \gamma whose underlying matrix satisfies the corresponding predicate; the coercion from the unit group to matrices is applied before testing the predicate. The four accompanying lemmas mem_centralCell_iff, mem_unipotentCell_iff, mem_hyperbolicCell_iff and mem_ellipticCell_iff record that membership in each cell is exactly the corresponding predicate on the underlying matrix, so that the set-builder definitions can be used interchangeably with the predicates. Note that the predicates are stated for arbitrary matrices and that no disjointness, exhaustiveness or conjugation-invariance statement is part of this module: it fixes the vocabulary only.

Relation to Mathlib

Mathlib supplies the characteristic polynomial Matrix.charpoly and the group GL (Fin 2) K used here, but has no classification of 2\times 2 matrices into central, unipotent, hyperbolic and elliptic types; these predicates and the four cells are the project's own.

Where it is used

The four cells give a partition of \mathrm{GL}_2 by the existence and multiplicity of rational eigenvalues, which is the division of conjugacy classes used on the geometric side of the \mathrm{GL}_2 trace formula and in the local analysis of automorphic forms on \mathrm{GL}_2. The vocabulary fixed here is used throughout the automorphic part of the development.

References

  1. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997
  2. S. Gelbart, Automorphic Forms on Adèle Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_AutomorphicForm_GL2ConjugacyCells.lean

Imports

  • only Mathlib

Imported by

Declarations

Source

import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff ↗
import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs ↗

set_option autoImplicit false

open Matrix Polynomial

noncomputable section

namespace AutomorphicForm

variable {K : Type*} [Field K]

def IsCentralType (M : Matrix (Fin 2) (Fin 2) K) : Prop :=
  ∃ c : K, M = c • (1 : Matrix (Fin 2) (Fin 2) K)

def IsUnipotentType (M : Matrix (Fin 2) (Fin 2) K) : Prop :=
  ¬IsCentralType M ∧ ∃ a : K, M.charpoly = (X - C a) ^ 2

def IsHyperbolicType (M : Matrix (Fin 2) (Fin 2) K) : Prop :=
  ∃ a b : K, a ≠ b ∧ M.charpoly = (X - C a) * (X - C b)

def IsEllipticType (M : Matrix (Fin 2) (Fin 2) K) : Prop :=
  ∀ a : K, ¬M.charpoly.IsRoot a

def centralCell (K : Type*) [Field K] : Set (GL (Fin 2) K) :=
  {γ | IsCentralType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K)}

def unipotentCell (K : Type*) [Field K] : Set (GL (Fin 2) K) :=
  {γ | IsUnipotentType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K)}

def hyperbolicCell (K : Type*) [Field K] : Set (GL (Fin 2) K) :=
  {γ | IsHyperbolicType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K)}

def ellipticCell (K : Type*) [Field K] : Set (GL (Fin 2) K) :=
  {γ | IsEllipticType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K)}

theorem mem_centralCell_iff {γ : GL (Fin 2) K} :
    γ ∈ centralCell K ↔ IsCentralType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K) :=
  Iff.rfl

theorem mem_unipotentCell_iff {γ : GL (Fin 2) K} :
    γ ∈ unipotentCell K ↔ IsUnipotentType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K) :=
  Iff.rfl

theorem mem_hyperbolicCell_iff {γ : GL (Fin 2) K} :
    γ ∈ hyperbolicCell K ↔ IsHyperbolicType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K) :=
  Iff.rfl

theorem mem_ellipticCell_iff {γ : GL (Fin 2) K} :
    γ ∈ ellipticCell K ↔ IsEllipticType ((γ : GL (Fin 2) K) : Matrix (Fin 2) (Fin 2) K) :=
  Iff.rfl

end AutomorphicForm

Statements phrased using this module (223)

… and 73 more statements (search for the module name to find them).