Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_WhittakerModelLocal.lean

definition module

Local Whittaker functions and spaces at places of

Throughout, F is a number field, \mathrm{GL}_2(\mathbb{A}_F) denotes AdelicGL2 (𝓞 F) F, pins : CarrierPins F is a bundle of auxiliary choices (a measurable space and a measure on \mathrm{GL}_2(\mathbb{A}_F), a set D, a subgroup Z of the ideles, a family U of subgroups indexed by ideals of \mathcal{O}_F, a family gen indexed by the finite places, and a measurable space and measure \nu on \mathbb{A}_F), and \psi is an additive character of \mathbb{A}_F with values in \mathbb{C}. For an arbitrary function \varphi : \mathrm{GL}_2(\mathbb{A}_F) \to \mathbb{C}, the global object used is its Whittaker coefficient of index \alpha = 1 \in F, namely g \mapsto \int_{\mathbb{A}_F} \varphi(\mathrm{unipotentGL2}(x)\, g)\,\psi(-(1 \cdot x))\,d\nu(x), the integral being taken against the measure \nu recorded in pins.

For a finite place v (a height-one prime of \mathcal{O}_F), localFnAt F pins ψ v φ is the function on \mathrm{GL}_2(F_v) sending g to the value of that Whittaker coefficient at the adelic point with v-component g, trivial component at every other finite place and trivial archimedean component; it is the composite of the monoid homomorphisms AdelicDock.localEmbed and AdelicDock.finEmbed followed by the Whittaker coefficient. Then localSpaceAt F pins ψ v φ is the \mathbb{C}-submodule of all functions \mathrm{GL}_2(F_v) \to \mathbb{C} spanned by the set of functions localFnAt F pins ψ v (fun x => φ (x * h)) as h ranges over \mathrm{GL}_2(\mathbb{A}_F), i.e. the span of the local restrictions of all right translates of \varphi. For an infinite place w, archFnAt and archSpaceAt are defined in exactly the same way, the one-place embedding \mathrm{GL}_2(F_w) \to \mathrm{GL}_2(\mathbb{A}_F) being NumberField.SiegelVolume.archEmbed. No linearity, invariance, integrability or continuity of \varphi is assumed; these are definitions for every \varphi. Four lemmas record the vanishing at \varphi = 0: the two restriction functions are identically zero, and the two spanned submodules are \bot.

Relation to Mathlib

Mathlib has no notion of Whittaker coefficients or Whittaker models of automorphic forms; these are the project's own definitions, built on Mathlib's adele ring, AddChar, adic and archimedean completions, and Submodule.span.

Where it is used

These definitions localise the global Whittaker expansion of a function on \mathrm{GL}_2(\mathbb{A}_F) place by place, producing at each place a complex vector space of functions on the local group; they form part of the adelic automorphic-forms layer on which the comparison between automorphic forms and Galois representations is set up.

References

  1. H. Jacquet and R. P. Langlands, Automorphic Forms on GL(2), Lecture Notes in Mathematics 114, Springer, 1970
  2. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997
  3. 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_AutomorphicForm_WhittakerModelLocal.lean

Imports

Imported by

Declarations

Source

import Definitions.Def_AutomorphicForm_WhittakerCoefficient
import Definitions.Def_AdelicDock_LocalEmbedding
import Definitions.Def_NumberField_SiegelVolume

set_option autoImplicit false

open NumberField IsDedekindDomain

namespace AutomorphicForm.WhittakerModel

variable (F : Type) [Field F] [NumberField F]

noncomputable def localFnAt (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (v : HeightOneSpectrum (𝓞 F)) (φ : AdelicGL2 (𝓞 F) F → ℂ) :
    GL (Fin 2) (v.adicCompletion F) → ℂ :=
  fun g => whittakerCoefficient F pins ψ φ 1
    (AdelicDock.finEmbed (𝓞 F) F (AdelicDock.localEmbed (𝓞 F) F v g))

noncomputable def localSpaceAt (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (v : HeightOneSpectrum (𝓞 F)) (φ : AdelicGL2 (𝓞 F) F → ℂ) :
    Submodule ℂ (GL (Fin 2) (v.adicCompletion F) → ℂ) :=
  Submodule.span ℂ
    {W | ∃ h : AdelicGL2 (𝓞 F) F, W = localFnAt F pins ψ v (fun x => φ (x * h))}

noncomputable def archFnAt (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (w : InfinitePlace F) (φ : AdelicGL2 (𝓞 F) F → ℂ) :
    GL (Fin 2) w.Completion → ℂ :=
  fun g => whittakerCoefficient F pins ψ φ 1 (NumberField.SiegelVolume.archEmbed F w g)

noncomputable def archSpaceAt (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (w : InfinitePlace F) (φ : AdelicGL2 (𝓞 F) F → ℂ) :
    Submodule ℂ (GL (Fin 2) w.Completion → ℂ) :=
  Submodule.span ℂ
    {W | ∃ h : AdelicGL2 (𝓞 F) F, W = archFnAt F pins ψ w (fun x => φ (x * h))}

variable {F}

@[simp] theorem localFnAt_zero (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (v : HeightOneSpectrum (𝓞 F)) :
    localFnAt F pins ψ v (fun _ => (0 : ℂ)) = fun _ => 0 :=
  funext fun _ => by simp only [localFnAt, whittakerCoefficient_zero]

@[simp] theorem archFnAt_zero (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (w : InfinitePlace F) :
    archFnAt F pins ψ w (fun _ => (0 : ℂ)) = fun _ => 0 :=
  funext fun _ => by simp only [archFnAt, whittakerCoefficient_zero]

theorem localSpaceAt_zero (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (v : HeightOneSpectrum (𝓞 F)) :
    localSpaceAt F pins ψ v (fun _ => (0 : ℂ)) = ⊥ := by
  refine Submodule.span_eq_bot.2 ?_
  rintro W ⟨h, rfl⟩
  funext g
  simp only [localFnAt, whittakerCoefficient_zero, Pi.zero_apply]

theorem archSpaceAt_zero (pins : CarrierPins F) (ψ : AddChar (AdeleRing (𝓞 F) F) ℂ)
    (w : InfinitePlace F) :
    archSpaceAt F pins ψ w (fun _ => (0 : ℂ)) = ⊥ := by
  refine Submodule.span_eq_bot.2 ?_
  rintro W ⟨h, rfl⟩
  funext g
  simp only [archFnAt, whittakerCoefficient_zero, Pi.zero_apply]

end AutomorphicForm.WhittakerModel

Statements phrased using this module (66)