Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_CubicInduction_LocalWhittakerDatum.lean

definition module

Local Whittaker datum for GL(3) at a finite place

Fix a finite place v of \mathbb{Q}, i.e. a point of the height-one spectrum of \mathcal{O}_{\mathbb{Q}}, an additive character \psi_v of the completion \mathbb{Q}_v with values in \mathbb{C}^\times (no condition on its conductor or nontriviality is imposed), and a function W on \mathrm{GL}_3(\mathbb{Q}_v) with complex values. The predicate IsLocalWhittakerDatum is the conjunction of six clauses. First, IsGL3PsiWhittakerFn for \psi_v: for all x,y,z\in\mathbb{Q}_v and all g, one has W(u(x,y,z)g)=\psi_v(x+y)W(g), where u(x,y,z) is the upper triangular unipotent matrix with superdiagonal entries x,y and corner entry z; thus the character is evaluated on the sum of the two superdiagonal entries, and for trivial \psi_v the clause degenerates to left invariance under the full unipotent radical. Second, W(1)=1. Third, HasWhittakerMultOne: writing V(W) for gl3CyclicSubspace W, the \mathbb{C}-span of all right translates h\mapsto W(hg) of W inside the space of all functions on \mathrm{GL}_3(\mathbb{Q}_v), and letting \mathrm{GL}_3(\mathbb{Q}_v) act on V(W) by right translation (gl3CyclicRep), the space of linear functionals L on V(W) satisfying L(\pi(u(x,y,z))f)=\psi_v(x+y)L(f) has rank at most 1. Fourth, an irreducibility clause phrased in terms of these cyclic spans: every nonzero F\in V(W) satisfies W\in V(F). Fifth, smoothness in the form of an open subgroup U_v\le \mathrm{GL}_3(\mathbb{Q}_v) with W(gk)=W(g) for all k\in U_v and all g. Sixth, admissibility: for every open subgroup U_v there is a finite set B of complex-valued functions on \mathrm{GL}_3(\mathbb{Q}_v) such that every F\in V(W) which is right U_v-invariant lies in the \mathbb{C}-span of B (the members of B are not themselves required to lie in V(W)).

Relation to Mathlib

Mathlib has no notion of Whittaker functions, Whittaker functionals or admissible smooth representations of p-adic groups; these are the project's own definitions, formulated using Mathlib's AddChar, general linear groups over adic completions, and Submodule.span.

Where it is used

The predicate pins down the local components at finite places of the Whittaker function of the \mathrm{GL}_3/\mathbb{Q} automorphic form produced by cubic induction, in the Langlands–Tunnell input to the modularity of the mod 3 representation attached to a Frey curve.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154
  2. H. Jacquet, I. I. Piatetski-Shapiro and J. A. Shalika, Automorphic forms on GL(3) I, II, Annals of Mathematics 109 (1979), 169–212 and 213–258
  3. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_LanglandsTunnell_CubicInduction_Structure

set_option autoImplicit false

noncomputable section

open IsDedekindDomain NumberField

namespace LanglandsTunnell.CubicInduction

def IsLocalWhittakerDatum (v : HeightOneSpectrum (𝓞 ℚ)) (ψv : AddChar (v.adicCompletion ℚ) ℂ)
    (W : LocalGL3 v → ℂ) : Prop :=
  IsGL3PsiWhittakerFn ψv W ∧ W 1 = 1 ∧
    HasWhittakerMultOne ψv W ∧
    (∀ F ∈ gl3CyclicSubspace W, F ≠ 0 → W ∈ gl3CyclicSubspace F) ∧
    (∃ Uv : Subgroup (LocalGL3 v), IsOpen (Uv : Set (LocalGL3 v)) ∧
      ∀ k ∈ Uv, ∀ g : LocalGL3 v, W (g * k) = W g) ∧
    ∀ Uv : Subgroup (LocalGL3 v), IsOpen (Uv : Set (LocalGL3 v)) →
      ∃ B : Finset (LocalGL3 v → ℂ), ∀ F ∈ gl3CyclicSubspace W,
        (∀ k ∈ Uv, ∀ g : LocalGL3 v, F (g * k) = F g) → F ∈ Submodule.span ℂ (B : Set (LocalGL3 v → ℂ))

end LanglandsTunnell.CubicInduction

end

Statements phrased using this module (6)