Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_AuxLevelHeckeModule.lean

definition module

Hecke datum and localised module at auxiliary level

Fix natural numbers N (nonzero) and r, a set S of natural numbers, and a commutative ring \mathcal O. The structure CuspForm.AuxLevel.Gen N r S is the index type whose terms consist of a natural number \ell together with proofs that \ell is prime, \ell \notin S, \ell \nmid N and \ell \neq r. The subgroup CuspForm.AuxLevel.subgroup N r of (\mathbb Z/Nr)^{\times} is the kernel of the reduction (\mathbb Z/Nr)^{\times}\to(\mathbb Z/r)^{\times}, so that the associated congruence subgroup \Gamma_H(Nr) is \Gamma_0(N)\cap\Gamma_1(r) in the project's formulation of \Gamma_H. The carrier Carrier N r π’ͺ is the corresponding raw cohomological carrier \operatorname{Hom}(\Gamma_H(Nr),\mathcal O), i.e. the \mathcal O-module of additive homomorphisms from the abelianised group to \mathcal O. For g of index type Gen, op N r S π’ͺ g is the endomorphism CohCarrier.heckeTL at the prime g.\ell: a homomorphism is restricted along conjugation by \operatorname{diag}(1,\ell) on \Gamma_H(Nr)\cap\Gamma^0(\ell) and then corestricted (by transfer) back to \Gamma_H(Nr). The predicate OpComm asserts that these endomorphisms commute pairwise.

Assuming in addition that \mathcal O is local, and given a ring homomorphism \theta from the weight-two Hecke algebra CuspForm.heckeAlgebra N 2 S (the \mathbb Z-subalgebra of \operatorname{End}_{\mathbb C} S_2(\Gamma_0(N)) generated by the T_\ell for primes \ell\nmid N, \ell\notin S and the U_q for primes q\mid N, q\notin S) to the residue field of \mathcal O, together with a proof hc of OpComm, heckeData assembles a CohCarrier.HeckeData: generators Gen N r S, operator family op, the commutation statement carried as the structure field comm, and residual values g\mapsto\theta(T_{g.\ell}). The instance instModuleFreeAlgCarrier records the resulting action of the free algebra \mathcal O[X_g] on the carrier through X_g\mapsto \mathrm{op}(g), and ML is the localisation of that module at the complement of the prime \ker\bigl(\mathcal O[X_g]\to \mathrm{ResidueField}\,\mathcal O,\ X_g\mapsto\theta(T_{g.\ell})\bigr); the closing examples record that this localisation is simultaneously a module over \mathcal O and over the free algebra, compatibly.

Relation to Mathlib

Mathlib supplies the ingredients β€” congruence subgroups, \mathbb C-valued cusp forms and their endomorphism algebra, ZMod.unitsMap, MvPolynomial, LocalizedModule and IsLocalRing.ResidueField β€” but the cohomological carriers \operatorname{Hom}(\Gamma_H(M),\mathcal O), the transfer-based Hecke operators on them and the notion of a Hecke datum are the project's own.

Where it is used

The module named ML here is the localised cohomology of the curve of level \Gamma_0(N)\cap\Gamma_1(r) at the maximal ideal attached to a residual eigensystem \theta; it is the base term of the Taylor–Wiles patching argument, whose companions at levels \Gamma_0(N)\cap\Gamma_1(rQ) for sets Q of Taylor–Wiles primes are compared with it. Only the operators indexed by primes \ell\notin S with \ell\nmid N and \ell\neq r enter the localisation.

References

  1. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, Β§3
  2. R. Taylor and A. Wiles, Ring-theoretic properties of certain Hecke algebras, Annals of Mathematics 141 (1995), 553–572

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

Imports

Imported by

Declarations

Source

import Definitions.Def_CohCarrier_Inst
import Definitions.Def_CuspForm_HeckeAlgebra
import Mathlib.RingTheory.LocalRing.ResidueField.Basic β†—

set_option autoImplicit false

noncomputable section

namespace CuspForm.AuxLevel

structure Gen (N r : β„•) (S : Set β„•) : Type where

  β„“ : β„•
  prime : β„“.Prime
  notMem : β„“ βˆ‰ S
  not_dvd : Β¬ β„“ ∣ N
  ne : β„“ β‰  r

def subgroup (N r : β„•) : Subgroup (ZMod (N * r))Λ£ :=
  (ZMod.unitsMap (dvd_mul_left r N)).ker

abbrev Carrier (N r : β„•) (π’ͺ : Type) [CommRing π’ͺ] : Type :=
  CohCarrier.H1 (N * r) (subgroup N r) π’ͺ

def op (N r : β„•) (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] (g : Gen N r S) :
    Module.End π’ͺ (Carrier N r π’ͺ) :=
  haveI : NeZero g.β„“ := ⟨g.prime.ne_zero⟩
  CohCarrier.heckeTL (N * r) (subgroup N r) π’ͺ g.β„“

def OpComm (N r : β„•) (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] : Prop :=
  βˆ€ g h : Gen N r S, op N r S π’ͺ g * op N r S π’ͺ h = op N r S π’ͺ h * op N r S π’ͺ g

def heckeData (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ]
    (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc : OpComm N r S π’ͺ) :
    CohCarrier.HeckeData π’ͺ (Carrier N r π’ͺ) (IsLocalRing.ResidueField π’ͺ) where
  Gen := Gen N r S
  op := op N r S π’ͺ
  comm := hc
  ΞΈbar g := ΞΈ (CuspForm.heckeAlgebra.T g.prime g.not_dvd g.notMem)

instance instModuleFreeAlgCarrier (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ]
    [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ)
    (hc : OpComm N r S π’ͺ) : Module (heckeData N r S π’ͺ ΞΈ hc).FreeAlg (Carrier N r π’ͺ) :=
  (heckeData N r S π’ͺ ΞΈ hc).moduleFreeAlg

abbrev ML (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ]
    (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc : OpComm N r S π’ͺ) : Type :=
  (heckeData N r S π’ͺ ΞΈ hc).ML

example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ]
    (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc : OpComm N r S π’ͺ) :
    Module π’ͺ (ML N r S π’ͺ ΞΈ hc) := by infer_instance

example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ]
    (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc : OpComm N r S π’ͺ) :
    Module (heckeData N r S π’ͺ ΞΈ hc).FreeAlg (ML N r S π’ͺ ΞΈ hc) := by infer_instance

example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ]
    (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc : OpComm N r S π’ͺ) :
    IsScalarTower π’ͺ (heckeData N r S π’ͺ ΞΈ hc).FreeAlg (ML N r S π’ͺ ΞΈ hc) := by infer_instance

end CuspForm.AuxLevel

end

Statements phrased using this module (9)