Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_AutomorphicForm_SmoothCuspRealization.lean

definition module

Smooth cuspidal realizations of Hecke eigensystems

Fix a number field F and write G = AdelicGL2 (π“ž F) F. The module first defines, for a tuple r : \mathrm{Fin}\,n \to G of representatives and \varphi : G \to \mathbb{C}, the coset sum SmoothCusp.heckeCosetSum = \sum_{i} \varphi(g\,r_i), records that it multiplies a constant function by n and is unchanged if each r_i is replaced by r_i u_i with u_i in a subgroup U under which \varphi is right invariant, and then defines SmoothCusp.IsHeckeCosetEigenfunctionAt U g_v v Ο† c: there exist \mathrm{N}v+1 elements of G forming an IsHeckeCosetSystem for (U, g_v) (the project's notion, from the imported Hecke coset module) whose coset sum satisfies \sum_i \varphi(g r_i) = c\,\varphi(g) for all g. The main definition is the structure SmoothCuspRealizationAt F pins Ξ¦, for a carrier bundle pins : CarrierPins F and a Hecke eigensystem \Phi with complex coefficients: it carries a function \varphi = toFun, a point where \varphi \ne 0, a character centralChar on the subgroup pins.Z, a proof that \varphi satisfies the project's predicate IsSmoothCuspAutomorphicFnAt for that bundle and character, right invariance of \varphi under pins.U Ξ¦.level, a finite exceptional set S of primes, and, for every v \notin S, both the coset eigenvalue equation with eigenvalue \Phi.a\,v at the generator pins.gen v and the central relation \varphi(\mathrm{diag}(\det(\mathrm{gen}\,v))\,g) = \Phi.b\,v\,\varphi(g). Realizability IsSmoothCuspRealizable is nonemptiness of this structure; smoothCuspNotionOf packages a field-indexed family of bundles into a CuspidalityNotion β„‚; IsSmoothCuspRealizableVia ΞΉ Ξ¦ applies it to \Phi.\mathrm{map}\,\iota for a ring map \iota : R \to \mathbb{C}. Derived lemmas: \varphi is left \mathrm{GL}_2(F)-invariant and IsKfSmooth; the central character is the ratio \varphi(zg)/\varphi(g) at any non-vanishing point and equals \Phi.b\,v when z = \det(\mathrm{gen}\,v); no coset eigenfunction exists at U = \top or U = \bot, so the level subgroup of a realization is neither. Finally an inhabitation section exhibits a degenerate bundle with zero measures and Z = \top, for which the constant function 1 is a realization of the degenerate eigensystem a_v = \mathrm{N}v + 1, b_v = 1, provided coset systems exist; this shows the notion is non-vacuous and imposes no archimedean type or minimal-level condition.

Relation to Mathlib

Mathlib has no notion of adelic automorphic form on \mathrm{GL}_2 or of Hecke eigensystem; all notions here are the project's own, built on Mathlib's adele ring, height-one spectrum, absolute ideal norm and measure theory.

Where it is used

This is the complex-analytic side of the correspondence: it supplies the target of the statement that a mod-\ell or \ell-adic Hecke eigensystem arising from a Galois representation is cuspidal, used when the eigensystem attached to the Frey curve is matched with an automorphic form. Many downstream modules of the tree take realizability at a bundle, in one of the three consumer forms given here, as their cuspidality hypothesis or conclusion.

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. S. Gelbart, Automorphic Forms on Adele Groups, Annals of Mathematics Studies 83, Princeton University Press, 1975
  3. D. Bump, Automorphic Forms and Representations, Cambridge Studies in Advanced Mathematics 55, Cambridge University Press, 1997

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

Imports

Imported by

Declarations

Source

import Definitions.Def_AutomorphicForm_SmoothAutomorphicFnAt
import Definitions.Def_AutomorphicForm_HeckeEigensystemMap
import Definitions.Def_LocalLanglands_HeckeCosetSystem

open IsDedekindDomain NumberField MeasureTheory Matrix
open AutomorphicForm HeckeIntegralSeam

noncomputable section

namespace AutomorphicForm

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

namespace SmoothCusp

def heckeCosetSum {n : β„•} (reps : Fin n β†’ AdelicGL2 (π“ž F) F)
    (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) (g : AdelicGL2 (π“ž F) F) : β„‚ :=
  βˆ‘ i, Ο† (g * reps i)

theorem heckeCosetSum_const {n : β„•} (reps : Fin n β†’ AdelicGL2 (π“ž F) F) (c : β„‚)
    (g : AdelicGL2 (π“ž F) F) :
    heckeCosetSum F reps (fun _ => c) g = (n : β„‚) * c := by
  simp [heckeCosetSum, Finset.sum_const, Finset.card_univ, nsmul_eq_mul]

theorem heckeCosetSum_mul_right {n : β„•} {U : Subgroup (AdelicGL2 (π“ž F) F)}
    {Ο† : AdelicGL2 (π“ž F) F β†’ β„‚}
    (hinv : βˆ€ g : AdelicGL2 (π“ž F) F, βˆ€ u ∈ U, Ο† (g * u) = Ο† g)
    (reps : Fin n β†’ AdelicGL2 (π“ž F) F) (u : Fin n β†’ AdelicGL2 (π“ž F) F)
    (hu : βˆ€ i, u i ∈ U) (g : AdelicGL2 (π“ž F) F) :
    heckeCosetSum F (fun i => reps i * u i) Ο† g = heckeCosetSum F reps Ο† g := by
  unfold heckeCosetSum
  congr 1; ext i
  rw [← mul_assoc]
  exact hinv (g * reps i) (u i) (hu i)

def IsHeckeCosetEigenfunctionAt (U : Subgroup (AdelicGL2 (π“ž F) F))
    (gv : AdelicGL2 (π“ž F) F) (v : HeightOneSpectrum (π“ž F))
    (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) (c : β„‚) : Prop :=
  βˆƒ reps : Fin (Ideal.absNorm v.asIdeal + 1) β†’ AdelicGL2 (π“ž F) F,
    IsHeckeCosetSystem U gv reps ∧
    βˆ€ g : AdelicGL2 (π“ž F) F, heckeCosetSum F reps Ο† g = c * Ο† g

end SmoothCusp

open SmoothCusp

structure SmoothCuspRealizationAt (pins : CarrierPins F) (Ξ¦ : HeckeEigensystem F β„‚) where
  toFun : AdelicGL2 (π“ž F) F β†’ β„‚
  exists_ne_zero : βˆƒ g : AdelicGL2 (π“ž F) F, toFun g β‰  0
  centralChar : pins.Z β†’* β„‚Λ£
  smoothCusp : IsSmoothCuspAutomorphicFnAt F pins centralChar toFun
  level_invariant : βˆ€ g : AdelicGL2 (π“ž F) F, βˆ€ u ∈ pins.U Ξ¦.level, toFun (g * u) = toFun g
  exceptionalSet : Finset (HeightOneSpectrum (π“ž F))
  hecke_eigen : βˆ€ v : HeightOneSpectrum (π“ž F), v βˆ‰ exceptionalSet β†’
    IsHeckeCosetEigenfunctionAt F (pins.U Ξ¦.level) (pins.gen v) v toFun (Ξ¦.a v)
  central_eigen : βˆ€ v : HeightOneSpectrum (π“ž F), v βˆ‰ exceptionalSet β†’
    βˆ€ g : AdelicGL2 (π“ž F) F,
      toFun (centralScalar (π“ž F) F (Matrix.GeneralLinearGroup.det (pins.gen v)) * g)
        = Ξ¦.b v * toFun g

def smoothCuspNotionOf
    (pins : βˆ€ (F : Type) [Field F] [NumberField F], CarrierPins F) :
    CuspidalityNotion β„‚ where
  IsCusp := fun F _i1 _i2 Ξ¦ => Nonempty (@SmoothCuspRealizationAt F _i1 _i2 (pins F) Ξ¦)

def IsSmoothCuspRealizable (pins : CarrierPins F) (Ξ¦ : HeckeEigensystem F β„‚) : Prop :=
  Nonempty (SmoothCuspRealizationAt F pins Ξ¦)

theorem isSmoothCuspRealizable_iff (pins : CarrierPins F) (Ξ¦ : HeckeEigensystem F β„‚) :
    IsSmoothCuspRealizable F pins Ξ¦ ↔ Nonempty (SmoothCuspRealizationAt F pins Ξ¦) := Iff.rfl

theorem smoothCuspNotionOf_isCusp_iff
    (pins : βˆ€ (F : Type) [Field F] [NumberField F], CarrierPins F)
    (Ξ¦ : HeckeEigensystem F β„‚) :
    (smoothCuspNotionOf pins).IsCusp F Ξ¦ ↔ IsSmoothCuspRealizable F (pins F) Ξ¦ := Iff.rfl

def IsSmoothCuspRealizableVia (pins : CarrierPins F) {R : Type*} [CommRing R]
    (ΞΉ : R β†’+* β„‚) (Ξ¦ : HeckeEigensystem F R) : Prop :=
  IsSmoothCuspRealizable F pins (Ξ¦.map ΞΉ)

theorem isSmoothCuspRealizableVia_id (pins : CarrierPins F) (Ξ¦ : HeckeEigensystem F β„‚) :
    IsSmoothCuspRealizableVia F pins (RingHom.id β„‚) Ξ¦ ↔ IsSmoothCuspRealizable F pins Ξ¦ := by
  unfold IsSmoothCuspRealizableVia; rw [HeckeEigensystem.map_id]

variable {F}

theorem SmoothCuspRealizationAt.toFun_ne_zero {pins : CarrierPins F}
    {Ξ¦ : HeckeEigensystem F β„‚} (R : SmoothCuspRealizationAt F pins Ξ¦) :
    R.toFun β‰  fun _ => 0 := by
  obtain ⟨g, hg⟩ := R.exists_ne_zero
  intro h; exact hg (congrFun h g)

theorem SmoothCuspRealizationAt.left_invariant {pins : CarrierPins F}
    {Ξ¦ : HeckeEigensystem F β„‚} (R : SmoothCuspRealizationAt F pins Ξ¦)
    (Ξ³ : GL (Fin 2) F) (g : AdelicGL2 (π“ž F) F) :
    R.toFun (globalPoints (π“ž F) F Ξ³ * g) = R.toFun g := by
  letI := pins.mS
  exact (((lsXiMemberAt_iff (π“ž F) F pins.ΞΌ pins.Z R.centralChar pins.D R.toFun).mp
    R.smoothCusp.1.1).1).left_invariant Ξ³ g

theorem SmoothCuspRealizationAt.isKfSmooth {pins : CarrierPins F}
    {Ξ¦ : HeckeEigensystem F β„‚} (R : SmoothCuspRealizationAt F pins Ξ¦) :
    IsKfSmooth F R.toFun :=
  R.smoothCusp.2

variable (F)

namespace SmoothCusp

theorem not_isHeckeCosetEigenfunctionAt_top (gv : AdelicGL2 (π“ž F) F)
    (v : HeightOneSpectrum (π“ž F)) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) (c : β„‚) :
    Β¬ IsHeckeCosetEigenfunctionAt F ⊀ gv v Ο† c := by
  rintro ⟨reps, hsys, -⟩
  haveI : Subsingleton (AdelicGL2 (π“ž F) F β§Έ (⊀ : Subgroup (AdelicGL2 (π“ž F) F))) :=
    QuotientGroup.subsingleton_quotient_top
  have hN : Ideal.absNorm v.asIdeal β‰  0 := Ideal.absNorm_eq_zero_iff.not.mpr v.ne_bot
  have h1 : 1 < Ideal.absNorm v.asIdeal + 1 := by omega
  have heq : (0 : Fin (Ideal.absNorm v.asIdeal + 1)) = ⟨1, h1⟩ :=
    hsys.mk_injective (Subsingleton.elim _ _)
  have : (0 : β„•) = 1 := congrArg Fin.val heq
  omega

theorem not_isHeckeCosetEigenfunctionAt_bot (gv : AdelicGL2 (π“ž F) F)
    (v : HeightOneSpectrum (π“ž F)) (Ο† : AdelicGL2 (π“ž F) F β†’ β„‚) (c : β„‚) :
    Β¬ IsHeckeCosetEigenfunctionAt F βŠ₯ gv v Ο† c := by
  rintro ⟨reps, hsys, -⟩
  have hall : βˆ€ i, reps i = gv := fun i => by
    obtain ⟨u, hu, w, hw, hx⟩ := HeckePair.mem_doubleCoset_iff.mp (hsys.mem_doubleCoset i)
    rw [Subgroup.mem_bot] at hu hw
    rw [hu, hw, one_mul, mul_one] at hx; exact hx.symm
  have hN : Ideal.absNorm v.asIdeal β‰  0 := Ideal.absNorm_eq_zero_iff.not.mpr v.ne_bot
  have h1 : 1 < Ideal.absNorm v.asIdeal + 1 := by omega
  have heq : (0 : Fin (Ideal.absNorm v.asIdeal + 1)) = ⟨1, h1⟩ := by
    apply hsys.mk_injective
    show QuotientGroup.mk (reps 0) = QuotientGroup.mk (reps ⟨1, h1⟩)
    rw [hall 0, hall ⟨1, h1⟩]
  have : (0 : β„•) = 1 := congrArg Fin.val heq
  omega

end SmoothCusp

variable {F}

theorem SmoothCuspRealizationAt.level_ne_top_ne_bot {pins : CarrierPins F}
    {Ξ¦ : HeckeEigensystem F β„‚} (R : SmoothCuspRealizationAt F pins Ξ¦)
    (v : HeightOneSpectrum (π“ž F)) (hv : v βˆ‰ R.exceptionalSet) :
    pins.U Ξ¦.level β‰  ⊀ ∧ pins.U Ξ¦.level β‰  βŠ₯ :=
  ⟨fun h => not_isHeckeCosetEigenfunctionAt_top F _ v _ _ (h β–Έ R.hecke_eigen v hv),
   fun h => not_isHeckeCosetEigenfunctionAt_bot F _ v _ _ (h β–Έ R.hecke_eigen v hv)⟩

example (pins : βˆ€ (F : Type) [Field F] [NumberField F], CarrierPins F) :
    CuspidalityNotion β„‚ := smoothCuspNotionOf pins

theorem SmoothCuspRealizationAt.centralChar_apply_eq {pins : CarrierPins F}
    {Ξ¦ : HeckeEigensystem F β„‚} (R : SmoothCuspRealizationAt F pins Ξ¦)
    (z : pins.Z) {g : AdelicGL2 (π“ž F) F} (hg : R.toFun g β‰  0) :
    ((R.centralChar z : β„‚Λ£) : β„‚) =
      R.toFun (centralScalar (π“ž F) F (z : (AdeleRing (π“ž F) F)Λ£) * g) / R.toFun g := by
  letI := pins.mS
  have ht := (((lsXiMemberAt_iff (π“ž F) F pins.ΞΌ pins.Z R.centralChar pins.D R.toFun).mp
    R.smoothCusp.1.1).1).central_transform z g
  rw [ht, mul_div_assoc, div_self hg, mul_one]

theorem SmoothCuspRealizationAt.centralChar_det_gen_eq_b {pins : CarrierPins F}
    {Ξ¦ : HeckeEigensystem F β„‚} (R : SmoothCuspRealizationAt F pins Ξ¦)
    {v : HeightOneSpectrum (π“ž F)} (hv : v βˆ‰ R.exceptionalSet) (z : pins.Z)
    (hz : (z : (AdeleRing (π“ž F) F)Λ£) = Matrix.GeneralLinearGroup.det (pins.gen v)) :
    ((R.centralChar z : β„‚Λ£) : β„‚) = Ξ¦.b v := by
  obtain ⟨g, hg⟩ := R.exists_ne_zero
  rw [R.centralChar_apply_eq z hg, hz, R.central_eigen v hv g, mul_div_assoc, div_self hg,
    mul_one]

section Inhabitor

variable (F)

def degenerateZeroMeasurePins (U : Ideal (π“ž F) β†’ Subgroup (AdelicGL2 (π“ž F) F))
    (gen : HeightOneSpectrum (π“ž F) β†’ AdelicGL2 (π“ž F) F) : CarrierPins F where
  mS := βŠ₯
  ΞΌ := 0
  D := Set.univ
  Z := ⊀
  U := U
  gen := gen
  nS := βŠ₯
  Ξ½ := 0

theorem isSmoothCuspAutomorphicFnAt_one_zeroMeasure
    (U : Ideal (π“ž F) β†’ Subgroup (AdelicGL2 (π“ž F) F))
    (gen : HeightOneSpectrum (π“ž F) β†’ AdelicGL2 (π“ž F) F) :
    IsSmoothCuspAutomorphicFnAt F (degenerateZeroMeasurePins F U gen)
      (1 : (⊀ : Subgroup (AdeleRing (π“ž F) F)Λ£) β†’* β„‚Λ£) (fun _ => (1 : β„‚)) := by
  refine ⟨⟨isAutomorphicFnAt_one_trivial F _ ?_, ?_⟩, isKfSmooth_const F 1⟩
  Β· have hΞΌ : (degenerateZeroMeasurePins F U gen).ΞΌ
        = (0 : @Measure _ (degenerateZeroMeasurePins F U gen).mS) := rfl
    rw [hΞΌ]; simp only [Measure.coe_zero, Pi.zero_apply]; exact ENNReal.zero_lt_top
  Β· intro g
    have hΞ½ : (degenerateZeroMeasurePins F U gen).Ξ½
        = (0 : @Measure _ (degenerateZeroMeasurePins F U gen).nS) := rfl
    rw [hΞ½]; unfold constantTerm; exact integral_zero_measure _

def degenerateEigensystem (N : Ideal (π“ž F)) (hN : N β‰  βŠ₯) : HeckeEigensystem F β„‚ where
  level := N
  level_ne_bot := hN
  a := fun v => ((Ideal.absNorm v.asIdeal : β„•) : β„‚) + 1
  b := fun _ => 1

@[simp] theorem degenerateEigensystem_a (N : Ideal (π“ž F)) (hN : N β‰  βŠ₯)
    (v : HeightOneSpectrum (π“ž F)) :
    (degenerateEigensystem F N hN).a v = ((Ideal.absNorm v.asIdeal : β„•) : β„‚) + 1 := rfl

@[simp] theorem degenerateEigensystem_b (N : Ideal (π“ž F)) (hN : N β‰  βŠ₯)
    (v : HeightOneSpectrum (π“ž F)) : (degenerateEigensystem F N hN).b v = 1 := rfl

def smoothCuspRealizationAt_one_of_cosetSystems
    (U : Ideal (π“ž F) β†’ Subgroup (AdelicGL2 (π“ž F) F))
    (gen : HeightOneSpectrum (π“ž F) β†’ AdelicGL2 (π“ž F) F) (N : Ideal (π“ž F)) (hN : N β‰  βŠ₯)
    (hsys : βˆ€ v : HeightOneSpectrum (π“ž F),
      βˆƒ reps : Fin (Ideal.absNorm v.asIdeal + 1) β†’ AdelicGL2 (π“ž F) F,
        IsHeckeCosetSystem (U N) (gen v) reps) :
    SmoothCuspRealizationAt F (degenerateZeroMeasurePins F U gen)
      (degenerateEigensystem F N hN) where
  toFun := fun _ => 1
  exists_ne_zero := ⟨1, one_ne_zero⟩
  centralChar := 1
  smoothCusp := isSmoothCuspAutomorphicFnAt_one_zeroMeasure F U gen
  level_invariant := fun _ _ _ => rfl
  exceptionalSet := βˆ…
  hecke_eigen := fun v _ => by
    obtain ⟨reps, hreps⟩ := hsys v
    refine ⟨reps, hreps, fun g => ?_⟩
    rw [heckeCosetSum_const, degenerateEigensystem_a, mul_one, mul_one]
    push_cast
    ring
  central_eigen := fun v _ g => by simp only [degenerateEigensystem_b, one_mul]

end Inhabitor

end AutomorphicForm

end

Statements phrased using this module (17)