Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_AdelicLift.lean

definition module

Adelic lift of a weight-two cusp form on

For a natural number M, a weight-two cusp form g on \mathrm{Gamma}_0(M) and a complex-valued function \varphi on the adelic group AutomorphicForm.AdelicGL2 (𝓞 ℚ) ℚ, the predicate CuspForm.IsAdelicLiftOf g φ is the conjunction of three conditions. First, left invariance under the rational points: \varphi(\iota(\gamma)x)=\varphi(x) for all \gamma\in\mathrm{GL}_2(\mathbb{Q}) and all x, where \iota is the embedding AutomorphicForm.globalPoints. Second, right invariance under the level subgroup: for every u in NumberField.AdelicLevel.finiteLevelOne (𝓞 ℚ) ℚ (AdelicDock.ratLevel M) and every x, \varphi(x\cdot\mathrm{finEmbed}(u))=\varphi(x). Here AdelicDock.ratLevel M is the ideal of \mathcal{O}_{\mathbb{Q}} generated by M; finiteLevelOne consists of those k\in\mathrm{GL}_2 over the finite adeles for which both k and k^{-1} have all entries integral at every finite place, lower-left entry of valuation at most the bound \exp(-\operatorname{ord}_v(N)) attached to the ideal N at each place v, and lower-right entry congruent to 1 to the same bound; AdelicDock.finEmbed inserts such a k into the adelic group with trivial archimedean component. Third, the archimedean normalisation: whenever the finite part AdelicLevel.glFin (𝓞 ℚ) ℚ h is trivial and the real component LanglandsTunnell.ratArchGL2 h lies in \mathrm{GL}_2^{+}(\mathbb{R}), one has \varphi(h)=\bigl(g\mid_2 \mathrm{ratArchGL2}(h)\bigr)(i), the weight-two slash action evaluated at i in the upper half-plane; no determinant factor occurs. The three accessor lemmas left_inv, level_inv and apply_eq extract the three conjuncts. This is a predicate on a given \varphi: neither existence nor uniqueness of a lift is asserted here.

Relation to Mathlib

Mathlib supplies the classical side (CuspForm, the weight-k slash action, Matrix.GLPos, UpperHalfPlane.I) but has no notion of the adelisation of a modular form; the adelic group, the finite-adelic level subgroups finiteLevelOne and the embeddings finEmbed, globalPoints, together with the real-component map ratArchGL2, are the project's own.

Where it is used

The predicate is the interface between classical weight-two cusp forms on \Gamma_0(M) and automorphic forms on \mathrm{GL}_2 over the adeles of \mathbb{Q}, so that Hecke eigenvalues and local conductors of the associated adelic object may be used; it feeds the modularity and level-lowering steps, where modular forms produced classically must be handled adelically.

References

  1. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997, §3.1
  2. S. Gelbart, Automorphic Forms on Adele 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_CuspForm_AdelicLift.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 IsAdelicLiftOf (g : CuspForm (CongruenceSubgroup.Gamma0 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 IsAdelicLiftOf.left_inv {g : CuspForm (CongruenceSubgroup.Gamma0 M) 2}
    {φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ} (hφg : IsAdelicLiftOf g φ)
    (γ : GL (Fin 2) ℚ) (x : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ) :
    φ (AutomorphicForm.globalPoints (NumberField.RingOfIntegers ℚ) ℚ γ * x) = φ x :=
  hφg.1 γ x

theorem IsAdelicLiftOf.level_inv {g : CuspForm (CongruenceSubgroup.Gamma0 M) 2}
    {φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ} (hφg : IsAdelicLiftOf 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 IsAdelicLiftOf.apply_eq {g : CuspForm (CongruenceSubgroup.Gamma0 M) 2}
    {φ : AutomorphicForm.AdelicGL2 (NumberField.RingOfIntegers ℚ) ℚ → ℂ} (hφg : IsAdelicLiftOf 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 (93)