Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_AdelicLiftGamma1.lean

definition module

Adelic lift of a weight-two cusp form on

Fix a natural number M, a cusp form g of weight 2 on \Gamma_1(M), and a function \varphi on the adelic group \mathrm{GL}_2(\mathbb{A}_{\mathbb{Q}}) (the group AutomorphicForm.AdelicGL2 attached to \mathcal{O}_{\mathbb{Q}} and \mathbb{Q}) with values in \mathbb{C}. The predicate CuspForm.IsAdelicLiftOfGamma1 g φ is the conjunction of three conditions. First, \varphi(\gamma x)=\varphi(x) for every \gamma\in\mathrm{GL}_2(\mathbb{Q}), pushed into the adelic group by AutomorphicForm.globalPoints, and every x. Second, \varphi(xu)=\varphi(x) for every x and every u in the image under AdelicDock.finEmbed (the embedding with trivial archimedean component) of the subgroup NumberField.AdelicLevel.finiteLevelOne of \mathrm{GL}_2 of the finite adeles at the ideal AdelicDock.ratLevel M =(M): that subgroup consists of those u for which both u and u^{-1} have all entries integral at every finite place, lower-left entry of valuation at most the bound attached to (M) at each place, and lower-right entry congruent to 1 in the same sense. Third, for every h whose finite part NumberField.AdelicLevel.glFin is trivial and whose real component LanglandsTunnell.ratArchGL2 h lies in Matrix.GLPos (Fin 2) ℝ, one has \varphi(h)=\bigl(g\mid_2 \mathrm{ratArchGL2}\,h\bigr)(i), the weight-2 slash action evaluated at i\in\mathfrak{H}.

The module is a predicate on a given pair (g,\varphi): no existence or uniqueness of a lift is asserted, nor anything about a central character. Three accompanying lemmas, left_inv, level_inv and apply_eq, are the projections onto the three clauses. No hypothesis M\neq 0 is imposed; for M=0 the ideal (M) is zero and the level subgroup degenerates accordingly.

Relation to Mathlib

The classical side uses Mathlib's CuspForm for CongruenceSubgroup.Gamma1 and Mathlib's weight-k slash action ∣[k]; the adelic side (the level subgroups, the finite/archimedean component maps and the embeddings) and the lifting predicate itself are the project's own notions, Mathlib having no adelic automorphic forms on \mathrm{GL}_2.

Where it is used

The predicate is the dictionary between weight-two cusp forms on \Gamma_1(M) and functions on \mathrm{GL}_2(\mathbb{A}_{\mathbb{Q}}), used where Hecke eigenvalue data of modular forms is transported to the adelic setting in the Langlands–Tunnell and modularity parts of the argument.

References

  1. S. Gelbart, Automorphic Forms on Adele Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975, §3
  2. I. Piatetski-Shapiro, Classical and adelic automorphic forms. An introduction, in: Automorphic Forms, Representations and L-functions, Proc. Sympos. Pure Math. 33, Part 1, American Mathematical Society, 1979, 185–188
  3. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997, Ch. 3

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_LanglandsTunnell_DeltaLift
import Definitions.Def_AdelicDock_LocalEmbedding

set_option autoImplicit false

noncomputable section

namespace CuspForm

variable {M : ℕ}

open scoped ModularForm in

def IsAdelicLiftOfGamma1 (g : CuspForm (CongruenceSubgroup.Gamma1 M) 2)
    (φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ) : Prop :=
  (∀ (γ : GL (Fin 2) ℚ) (x : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ),
      φ (AutomorphicForm.globalPoints (NumberField.RingOfIntegers ℚ) ℚ γ * x) = φ x) ∧
    (∀ u ∈ NumberField.AdelicLevel.finiteLevelOne (NumberField.RingOfIntegers ℚ) ℚ (AdelicDock.ratLevel M),
      ∀ x, φ (x * AdelicDock.finEmbed (NumberField.RingOfIntegers ℚ) ℚ u) = φ x) ∧
    ∀ h : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ,
      NumberField.AdelicLevel.glFin (NumberField.RingOfIntegers ℚ) ℚ h = 1 →
        LanglandsTunnell.ratArchGL2 h ∈ Matrix.GLPos (Fin 2) ℝ →
          φ h = ((⇑g) ∣[(2 : ℤ)] LanglandsTunnell.ratArchGL2 h) UpperHalfPlane.I

theorem IsAdelicLiftOfGamma1.left_inv {g : CuspForm (CongruenceSubgroup.Gamma1 M) 2}
    {φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ} (hφg : IsAdelicLiftOfGamma1 g φ)
    (γ : GL (Fin 2) ℚ) (x : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ) :
    φ (AutomorphicForm.globalPoints (NumberField.RingOfIntegers ℚ) ℚ γ * x) = φ x :=
  hφg.1 γ x

theorem IsAdelicLiftOfGamma1.level_inv {g : CuspForm (CongruenceSubgroup.Gamma1 M) 2}
    {φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ} (hφg : IsAdelicLiftOfGamma1 g φ) :
    ∀ u ∈ NumberField.AdelicLevel.finiteLevelOne (NumberField.RingOfIntegers ℚ) ℚ (AdelicDock.ratLevel M),
      ∀ x, φ (x * AdelicDock.finEmbed (NumberField.RingOfIntegers ℚ) ℚ u) = φ x :=
  hφg.2.1

open scoped ModularForm in

theorem IsAdelicLiftOfGamma1.apply_eq {g : CuspForm (CongruenceSubgroup.Gamma1 M) 2}
    {φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ} (hφg : IsAdelicLiftOfGamma1 g φ)
    (h : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ)
    (hfin : NumberField.AdelicLevel.glFin (NumberField.RingOfIntegers ℚ) ℚ h = 1)
    (hpos : LanglandsTunnell.ratArchGL2 h ∈ Matrix.GLPos (Fin 2) ℝ) :
    φ h = ((⇑g) ∣[(2 : ℤ)] LanglandsTunnell.ratArchGL2 h) UpperHalfPlane.I :=
  hφg.2.2 h hfin hpos

end CuspForm

end

Statements phrased using this module (39)