Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_AuxLevelHeckeModuleMid.lean

definition module

Intermediate-level Hecke datum and its localised module

Throughout, N\ge 1 and r are natural numbers, S a set of natural numbers, and \mathcal O a commutative (later local) ring. The carrier is CohCarrier.H1 (N * r) ⊀ π’ͺ, that is the group of additive homomorphisms from \Gamma_0(Nr) to \mathcal O (the project's GammaH (N*r) ⊀ is \Gamma_0(Nr)), with its natural \mathcal O-module structure; the sublevel \top distinguishes this intermediate level from the auxiliary level subgroup N r used for Carrier N r π’ͺ. A generator is an element of the project structure Gen N r S: a natural number \ell together with proofs that \ell is prime, \ell\notin S, \ell\nmid N and \ell\ne r. For such a generator, midOp N r S π’ͺ g is the \mathcal O-linear endomorphism CohCarrier.heckeTL (N*r) ⊀ π’ͺ g.β„“ of the carrier: a homomorphism \varphi is first pulled back along the conjugation map \gamma\mapsto\begin{pmatrix}a&b/\ell\\ c\ell&d\end{pmatrix} from \Gamma_0(Nr)\cap\Gamma^0(\ell) to \Gamma_0(Nr), and then pushed forward by the additive transfer coresAdd of that finite-index subgroup. The predicate MidOpComm N r S π’ͺ asserts that these operators commute pairwise.

Given a local ring \mathcal O, a ring homomorphism \theta from the weight-two level-N Hecke algebra CuspForm.heckeAlgebra N 2 S (the \mathbb Z-subalgebra of \mathrm{End}_{\mathbb C}S_2(\Gamma_0(N)) generated by the T_\ell with \ell prime, \ell\nmid N, \ell\notin S and the U_q with q prime, q\mid N, q\notin S) to the residue field of \mathcal O, and a proof hc₁ of commutativity, midHeckeData packages these into a CohCarrier.HeckeData: generators Gen N r S, operators midOp, the commutativity proof as a field, and residual eigenvalues g\mapsto\theta(T_{g.\ell}). The associated free algebra is the polynomial ring \mathcal O[X_g] over these generators, acting on the carrier through X_g\mapsto \mathrm{midOp}\,g (the instance instModuleFreeAlgMidCarrier), and midML is the localisation of the carrier at the complement of the prime ideal \ker(X_g\mapsto\theta(T_{g.\ell})), an \mathcal O-module and a module over the free algebra, compatibly. Further observations record that the free algebra and this prime ideal are literally those attached to the auxiliary-level datum heckeData for the same \theta.

Relation to Mathlib

The cohomology carrier, the transfer-based Hecke operators and the HeckeData packaging are the project's own; the free algebra and the localisation are Mathlib's MvPolynomial and LocalizedModule, and the residue field is Mathlib's IsLocalRing.ResidueField.

Where it is used

These definitions provide the Hecke module at the intermediate level \Gamma_0(Nr), localised at the residual eigensystem cut out by \theta, to be compared with the corresponding modules at level \Gamma_0(N) and at the auxiliary level between them; such comparisons of localised Hecke modules as the level is raised by an auxiliary prime r underlie the level-changing arguments in the modularity route to Fermat's Last Theorem.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Definitions.Def_CuspForm_AuxLevelHeckeModule

set_option autoImplicit false

noncomputable section

namespace CuspForm.AuxLevel

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

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

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

instance instModuleFreeAlgMidCarrier (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ]
    [IsLocalRing π’ͺ] (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ)
    (hc₁ : MidOpComm N r S π’ͺ) :
    Module (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg (CohCarrier.H1 (N * r) ⊀ π’ͺ) :=
  (midHeckeData N r S π’ͺ ΞΈ hc₁).moduleFreeAlg

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

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

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

example (N r : β„•) [NeZero N] (S : Set β„•) (π’ͺ : Type) [CommRing π’ͺ] [IsLocalRing π’ͺ]
    (ΞΈ : β†₯(CuspForm.heckeAlgebra N 2 S) β†’+* IsLocalRing.ResidueField π’ͺ) (hc₁ : MidOpComm N r S π’ͺ) :
    Module π’ͺ (midML 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₁ : MidOpComm N r S π’ͺ) :
    Module (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg (midML 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₁ : MidOpComm N r S π’ͺ) :
    IsScalarTower π’ͺ (midHeckeData N r S π’ͺ ΞΈ hc₁).FreeAlg (midML N r S π’ͺ ΞΈ hc₁) := by infer_instance

end CuspForm.AuxLevel

end

Statements phrased using this module (2)