Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_CubicInduction_SpectralOperators3.lean

definition module

Spectral operators on the GL₃ cuspidal slab L² space

Throughout, \omega is a character of the idele units of \mathbb{Q} with values in \mathbb{C}^\times, a,b are reals and \Phi_0 is a subset of \mathrm{GL}_3 of the adeles of \mathbb{Q}; cuspidalSubspace ω a b Φ₀ is the closure of the span of the images under toL2 of the cusp functions inside L^2 of the Haar measure on \mathrm{GL}_3(\mathbb{A}_\mathbb{Q}) restricted to the slab \{a \le \|\det g\| \le b\} and then to \Phi_0. Four notions are introduced. First, IsSpectralTranslation3 h holds when either the archimedean component of h is trivial (i.e. h lies in the kernel of archComponent3), or all finite components componentAt3 p h equal 1 and the archimedean component matrix k over the infinite adele ring satisfies k^{\mathsf T}k = 1. Second, for an operation op on complex-valued functions on \mathrm{GL}_3(\mathbb{A}_\mathbb{Q}) and a continuous linear endomorphism T of the cuspidal subspace, IsCuspLift3 asserts that for every F in cuspFunctions ω a b Φ₀ the function op F again lies in cuspFunctions ω a b Φ₀ and T carries the class of F in the cuspidal subspace to the class of op F; so T is determined on cusp classes by op. Third, spectralGenerators3 is the union of the set of those T that lift right translation translateRight h by some spectral translation h and the set of those T that lift smoothingOperator φ for some \varphi satisfying IsSmoothingKernel. Finally, spectralOperators3 adjoins to the generators every T for which some generator S satisfies \langle Tx, y\rangle = \langle x, Sy\rangle for all x,y in the cuspidal subspace, so the resulting set contains adjoints of generators.

Relation to Mathlib

The L^2 space, its inner product and continuous linear maps are Mathlib's; the adelic and automorphic notions (spectral translations, smoothing kernels, cusp functions, cuspidal subspace) are the project's own. The adjoint condition is stated directly through inner products rather than via Mathlib's ContinuousLinearMap.adjoint.

Where it is used

These operator families are part of the cubic-induction construction that supplies the Langlands–Tunnell input: a commuting family of translation and smoothing operators acting on the cuspidal part of an L^2 slab for \mathrm{GL}_3 over \mathbb{Q}, closed under adjoints, which is what the spectral analysis of the automorphic form produced by induction from a cubic field requires. Langlands–Tunnell in turn gives modularity of the mod 3 representation attached to an elliptic curve, the starting point of the Frey curve argument for Fermat's Last Theorem.

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. H. Jacquet, I. I. Piatetski-Shapiro and J. A. Shalika, Automorphic forms on GL(3), I and II, Annals of Mathematics 109 (1979), 169–212 and 213–258

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_LanglandsTunnell_CubicInduction_SlabL2Cusp

open NumberField IsDedekindDomain Matrix
open scoped InnerProductSpace

namespace LanglandsTunnell.CubicInduction.SlabL2

def IsSpectralTranslation3 (h : AdelicGL 3 (𝓞 ℚ) ℚ) : Prop :=
  h ∈ (archComponent3 (𝓞 ℚ) ℚ).ker ∨
    ((∀ p : HeightOneSpectrum (𝓞 ℚ), componentAt3 (𝓞 ℚ) ℚ p h = 1) ∧
      (archComponent3 (𝓞 ℚ) ℚ h : Matrix (Fin 3) (Fin 3) (InfiniteAdeleRing ℚ))ᵀ *
          (archComponent3 (𝓞 ℚ) ℚ h : Matrix (Fin 3) (Fin 3) (InfiniteAdeleRing ℚ)) = 1)

def IsCuspLift3 (ω : (AdeleRing (𝓞 ℚ) ℚ)ˣ →* ℂˣ) (a b : ℝ) (Φ₀ : Set (AdelicGL 3 (𝓞 ℚ) ℚ))
    (op : (AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) → (AdelicGL 3 (𝓞 ℚ) ℚ → ℂ))
    (T : ↥(cuspidalSubspace ω a b Φ₀) →L[ℂ] ↥(cuspidalSubspace ω a b Φ₀)) : Prop :=
  ∀ (F : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ) (hF : F ∈ cuspFunctions ω a b Φ₀),
    ∃ hRF : op F ∈ cuspFunctions ω a b Φ₀,
      (T ⟨toL2 ω a b Φ₀ ⟨F, hF.1⟩, toL2_mem_cuspidalSubspace_of_mem_cuspFunctions ω a b Φ₀ hF⟩ : Carrier a b Φ₀) =
        toL2 ω a b Φ₀ ⟨op F, hRF.1⟩

def spectralGenerators3 (ω : (AdeleRing (𝓞 ℚ) ℚ)ˣ →* ℂˣ) (a b : ℝ) (Φ₀ : Set (AdelicGL 3 (𝓞 ℚ) ℚ)) :
    Set (↥(cuspidalSubspace ω a b Φ₀) →L[ℂ] ↥(cuspidalSubspace ω a b Φ₀)) :=
  {T | ∃ h : AdelicGL 3 (𝓞 ℚ) ℚ, IsSpectralTranslation3 h ∧ IsCuspLift3 ω a b Φ₀ (translateRight h) T} ∪
    {T | ∃ φ : AdelicGL 3 (𝓞 ℚ) ℚ → ℂ, IsSmoothingKernel φ ∧ IsCuspLift3 ω a b Φ₀ (smoothingOperator φ) T}

def spectralOperators3 (ω : (AdeleRing (𝓞 ℚ) ℚ)ˣ →* ℂˣ) (a b : ℝ) (Φ₀ : Set (AdelicGL 3 (𝓞 ℚ) ℚ)) :
    Set (↥(cuspidalSubspace ω a b Φ₀) →L[ℂ] ↥(cuspidalSubspace ω a b Φ₀)) :=
  spectralGenerators3 ω a b Φ₀ ∪
    {T | ∃ S ∈ spectralGenerators3 ω a b Φ₀,
      ∀ x y : ↥(cuspidalSubspace ω a b Φ₀), ⟪T x, y⟫_ℂ = ⟪x, S y⟫_ℂ}

end LanglandsTunnell.CubicInduction.SlabL2

Statements phrased using this module (6)