Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_CubicInduction_ArchCentre3.lean

definition module

Casimir operators and centre-finiteness for adelic GL₃ forms

Fix the group G = AdelicGL 3 (𝓞 ℚ) ℚ = \mathrm{GL}_3 of the adele ring of \mathbb{Q}, and consider complex-valued functions \varphi on it. The first definition, archDeriv i j φ, takes indices i,j \in \{0,1,2\} and produces the function sending g to the derivative at s = 0 of the real-variable function s \mapsto \varphi\bigl(g \cdot \mathrm{archRealLift3}(\delta + s E_{ij})\bigr), where \delta + sE_{ij} is the real 3\times 3 matrix whose (a,b) entry is 1 if a=b plus s if (a,b) = (i,j), and archRealLift3 places a real matrix at the archimedean component of the adeles with identity finite part, returning the corresponding element of \mathrm{GL}_3(\mathbb{A}) when that adelic matrix is a unit and 1 otherwise. Thus archDeriv i j is right differentiation along the elementary matrix E_{ij} at the infinite place.

Three operators are then built from these directional derivatives: casimir1 φ = ∑_i archDeriv i i φ, casimir2 φ = ∑_{i,j} archDeriv i j (archDeriv j i φ) and casimir3 φ = ∑_{i,j,k} archDeriv i j (archDeriv j k (archDeriv k i φ)), the images of the symmetric expressions \sum_i E_{ii}, \sum_{i,j} E_{ij}E_{ji} and \sum_{i,j,k} E_{ij}E_{jk}E_{ki} in the universal enveloping algebra of \mathfrak{gl}_3.

Finally, IsCentreFinite φ is the conjunction, for each of the three operators T \in \{casimir1, casimir2, casimir3\}, of the assertion that there exist N \in \mathbb{N} and coefficients a : \mathrm{Fin}(N+1) \to \mathbb{C} with a_N = 1 such that \sum_{m} a_m \cdot T^{m}(\varphi) = 0 as a function on G, the iterates being ordinary function iteration. So centre-finiteness is formulated as a monic polynomial relation, separately in each of the three chosen operators, rather than as finiteness of the module generated by the whole centre.

Relation to Mathlib

Mathlib has no notion of automorphic forms on adelic \mathrm{GL}_n or of Casimir operators acting on them; these definitions are the project's own, built from Mathlib's deriv and adele-ring constructions.

Where it is used

These are the archimedean conditions in the project's vocabulary for automorphic forms on \mathrm{GL}_3 over \mathbb{Q}, used in the treatment of cubic induction underlying the Langlands–Tunnell input, which supplies modularity of the mod-3 representation attached to a Frey curve.

References

  1. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
  2. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175
  3. A. Borel and H. Jacquet, Automorphic forms and automorphic representations, in: Automorphic Forms, Representations and L-functions, Proceedings of Symposia in Pure Mathematics 33, American Mathematical Society, 1979, 189–207

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_LanglandsTunnell_CubicInduction_ArchCentre3.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_LanglandsTunnell_CubicInduction_ArchSmooth3

set_option autoImplicit false

noncomputable section

open IsDedekindDomain NumberField AutomorphicForm

namespace LanglandsTunnell.CubicInduction.WhittakerBlock

def archDeriv (i j : Fin 3) (φ : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ :=
  fun g => deriv (fun s : ℝ => φ (g * WhittakerBlock.archRealLift3 fun a b =>
    (if a = b then (1 : ℝ) else 0) + if a = i ∧ b = j then s else 0)) 0

def casimir1 (φ : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ :=
  fun g => ∑ i : Fin 3, archDeriv i i φ g

def casimir2 (φ : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ :=
  fun g => ∑ i : Fin 3, ∑ j : Fin 3, archDeriv i j (archDeriv j i φ) g

def casimir3 (φ : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ :=
  fun g => ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, archDeriv i j (archDeriv j k (archDeriv k i φ)) g

def IsCentreFinite (φ : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) : Prop :=
  (∃ (N : ℕ) (a : Fin (N + 1) → ℂ), a (Fin.last N) = 1 ∧ ∑ m, a m • (casimir1^[m] φ) = 0) ∧
    (∃ (N : ℕ) (a : Fin (N + 1) → ℂ), a (Fin.last N) = 1 ∧ ∑ m, a m • (casimir2^[m] φ) = 0) ∧
      ∃ (N : ℕ) (a : Fin (N + 1) → ℂ), a (Fin.last N) = 1 ∧ ∑ m, a m • (casimir3^[m] φ) = 0

end LanglandsTunnell.CubicInduction.WhittakerBlock

Statements phrased using this module (210)

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