Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_LanglandsTunnell_OctahedralDatum.lean

definition module

Carriers for Langlands–Tunnell: octahedral Galois data and their Hecke eigensystems

Two structures and two propositions. OctahedralGaloisDatum F R, for a number field F and a commutative ring R, packages: a type G carrying Group and Finite instances, a monoid homomorphism proj : G →* Equiv.Perm (Fin 4) together with a proof that it is surjective, and a field attached : HeckeEigensystem F R. Nothing in this structure relates G to \mathrm{Gal}(\bar F/F) or relates attached to proj: G is an abstract finite group with a surjection onto S_4, and the eigensystem is free data. TunnellOctahedralGlobal notion, for a CuspidalityNotion R (the project's abstract parameter for what cuspidality means on Hecke eigensystems), asserts that for every number field F and every such datum D there is \pi : HeckeEigensystem F R with notion.IsCusp F π and HeckeEigensystem.AgreesAwayFromFinite π D.attached, i.e. \pi is cuspidal in the chosen sense and agrees with the attached data outside a finite set of primes.

OctahedralGaloisDatumLinked extends the above by data tying attached to an actual two-dimensional representation: rep : G →* GL (Fin 2) R; the requirement rep_proj that for each g, \mathrm{proj}(g)=1 holds exactly when the matrix of rep g is a scalar c\cdot 1 with c \in R^\times (so \ker(\mathrm{proj}) is the locus where rep is scalar — only this kernel condition is imposed, not that proj is induced by rep); an arbitrary function frob from the height-one spectrum of \mathcal O_F to G, otherwise unconstrained; a finite set ramified of primes; and the identities attached.a v = trace (rep (frob v)), attached.b v = det (rep (frob v)) for every v \notin ramified. TunnellOctahedralGlobalLinked notion is the same existence assertion for linked data. Both propositions are shaped as universal statements over abstract data rather than over Galois representations, so they are formally stronger and differently shaped than Tunnell's theorem.

Relation to Mathlib

Mathlib has no notion of automorphic representation, Hecke eigensystem or Artin representation; HeckeEigensystem, CuspidalityNotion and AgreesAwayFromFinite are the project's own, from the imported definition modules. Mathlib supplies only the ambient objects used here: Equiv.Perm (Fin 4), GL (Fin 2) R, and IsDedekindDomain.HeightOneSpectrum (𝓞 F).

Where it is used

These carriers hold the Langlands–Tunnell input to the Frey–Serre–Ribet–Wiles argument: the statement that a two-dimensional Galois representation of octahedral projective type is matched, away from finitely many places, by a cuspidal Hecke eigensystem, which is what makes the residual mod 3 representation of a Frey curve modular. Two statement modules of the tree import this module.

References

  1. J. Tunnell, Artin's conjecture for representations of octahedral type, Bulletin of the American Mathematical Society (N.S.) 5 (1981), 173–175
  2. R. P. Langlands, Base Change for GL(2), Annals of Mathematics Studies 96, Princeton University Press, 1980
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Imported by

Declarations

Source

import Mathlib
import Definitions.Def_AutomorphicForm_HeckeEigensystem
import Definitions.Def_LanglandsTunnell_ExplicitLift

set_option autoImplicit false

open AutomorphicForm IsDedekindDomain NumberField
open scoped MatrixGroups

namespace FLT.TunnellOctahedralGlobalCarrier

structure OctahedralGaloisDatum (F : Type) [Field F] [NumberField F]
    (R : Type*) [CommRing R] where

  G : Type

  [grp : Group G]

  [fin : Finite G]

  proj : G →* Equiv.Perm (Fin 4)

  proj_surjective : Function.Surjective proj

  attached : HeckeEigensystem F R

attribute [instance] OctahedralGaloisDatum.grp OctahedralGaloisDatum.fin

def TunnellOctahedralGlobal {R : Type*} [CommRing R] (notion : CuspidalityNotion R) : Prop :=
  ∀ (F : Type) [Field F] [NumberField F],
    ∀ D : OctahedralGaloisDatum F R,
      ∃ π : HeckeEigensystem F R,
        notion.IsCusp F π ∧ HeckeEigensystem.AgreesAwayFromFinite π D.attached

end FLT.TunnellOctahedralGlobalCarrier

namespace FLT.Qepw139bOctahedralDatumLinkedRecarve

open FLT.TunnellOctahedralGlobalCarrier

structure OctahedralGaloisDatumLinked (F : Type) [Field F] [NumberField F]
    (R : Type*) [CommRing R] extends OctahedralGaloisDatum F R where

  rep : G →* GL (Fin 2) R

  rep_proj : ∀ g : G, proj g = 1 ↔
    ∃ c : Rˣ, ((rep g : GL (Fin 2) R) : Matrix (Fin 2) (Fin 2) R) = (c : R) • 1

  frob : HeightOneSpectrum (𝓞 F) → G

  ramified : Finset (HeightOneSpectrum (𝓞 F))

  attached_a : ∀ v ∉ ramified,
    attached.a v = ((rep (frob v) : GL (Fin 2) R) : Matrix (Fin 2) (Fin 2) R).trace

  attached_b : ∀ v ∉ ramified,
    attached.b v = ((rep (frob v) : GL (Fin 2) R) : Matrix (Fin 2) (Fin 2) R).det

def TunnellOctahedralGlobalLinked {R : Type*} [CommRing R]
    (notion : CuspidalityNotion R) : Prop :=
  ∀ (F : Type) [Field F] [NumberField F],
    ∀ D : OctahedralGaloisDatumLinked F R,
      ∃ π : HeckeEigensystem F R,
        notion.IsCusp F π ∧ HeckeEigensystem.AgreesAwayFromFinite π D.attached

end FLT.Qepw139bOctahedralDatumLinkedRecarve

Statements phrased using this module (0)

No statement module imports it directly (it is used through other definition modules or by proofs).