Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_SSHeckeV2.lean

definition module

Supersingular Hecke operator, lifting map, q-expansion restriction

Throughout, p\ge 5 is a prime, N a level, K an algebraically closed field of characteristic p, and F=\,modularFunctionFieldC K N the K-subfield of K((q)) generated by j(q) and j(q^{N}); for a prime \ell the roof R=\,charLDegeneracyRoof K N ℓ is the subfield generated by j(q),j(q^{N}),j(q^{\ell}),j(q^{N\ell}), with the two legs \alpha=\,heckeAlphaC (inclusion F\subseteq R) and \beta=\,heckeBetaC (the substitution q\mapsto q^{\ell} on q-expansions).

heckeMultiplier is an element h of R, chosen by Classical.epsilon, satisfying the differential identity d(\beta(\bar j))=h\cdot \mathrm{map}_{\alpha}\bigl(d\bar j\bigr) in \Omega_{R/K}, where \bar j=\,jGeomGen K N is j(q), R carries the F-algebra structure along \alpha, and \mathrm{map}_{\alpha}:\Omega_{F/K}\to\Omega_{R/K} is the functorial map; if no such element exists the choice is unconstrained.

liftFun hp5 k v, for k\in\mathbb Z and v in the carrier SSCarrier p N K hp5 k (a K-valued function on the supersingular index set), is an epsilon-chosen g\in F subject to two conditions: at every place z\in\,ssPlaces p N K one has \operatorname{ord}_z g\ge -\,weightDivisor K N (k/2).toNat (z), and for every index x the leading coefficient lead N K x.1 (poleOrder … x) g equals v\,x.

ssHeckeFun hp5 k ℓ v is again a carrier element: its value at x is \ell^{\,k/2-1} (in K) times the leading coefficient, in the same normalisation poleOrder … x, of \operatorname{Tr}_{R/F}\bigl(\beta(\mathrm{liftFun}\,v)\cdot h^{(k/2).\mathrm{toNat}}\bigr), the trace being taken for the F-algebra structure on R along \alpha.

resQFun hp5 k φ, for a power series \varphi over K, sends x to the leading coefficient at x (same pole normalisation) of an epsilon-chosen G\in F whose Laurent series equals \varphi\cdot\bigl(\theta(j(q))\bigr)^{-(k/2)}, where \theta(f)=q\,df/dq is thetaL.

Relation to Mathlib

Kähler differentials and their functorial maps, Algebra.trace, and Laurent/power series come from Mathlib; the modular function field, the degeneracy roof with its two legs, the supersingular carrier with its pole orders and leading coefficients, the weight divisor and the operator \theta are the project's own notions, and Mathlib has no Hecke action on functions on supersingular points.

Where it is used

These definitions set up the Hecke action on K-valued functions on the supersingular points of X_0(N) in characteristic p, together with the passage from mod-p q-expansions of weight k to such functions; this module is the computational input for the mod-p comparison of Hecke eigensystems that underlies the level-lowering step of the Frey–Serre–Ribet argument.

References

  1. J.-P. Serre, Sur les représentations modulaires de degré 2 de \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), Duke Mathematical Journal 54 (1987), 179–230
  2. K. A. Ribet, On modular representations of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) arising from modular forms, Inventiones Mathematicae 100 (1990), 431–476

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib
import Definitions.Def_ModularCurve_PlaceWidth
import Definitions.Def_ModularCurve_CharLDegeneracyHecke
import Definitions.Def_ModularCurve_QExpansionDiff
import Definitions.Def_AlgebraicCurve_Correspondence
import Definitions.Def_ModularCurve_CharLSpecialFibreLevelNDictionary
import Definitions.Def_ModularCurve_WeightDivisor
import Definitions.Def_ModularCurve_SSCarrier

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

noncomputable section
open AlgebraicCurve ModularCurve

namespace ModularCurve
variable (p : ℕ) [Fact p.Prime] (N : ℕ) [NeZero N] (K : Type) [Field K] [CharP K p] [IsAlgClosed K] [DecidableEq K]

def heckeMultiplier (ℓ : ℕ) [NeZero ℓ] : ↥(charLDegeneracyRoof K N ℓ) :=
  Classical.epsilon (fun h : ↥(charLDegeneracyRoof K N ℓ) =>
    letI := AlgebraicCurve.algebraAlong (heckeAlphaC K N ℓ)
    haveI := AlgebraicCurve.isScalarTower_along (heckeAlphaC K N ℓ)
    KaehlerDifferential.D K ↥(charLDegeneracyRoof K N ℓ) (heckeBetaC K N ℓ (jGeomGen K N))
      = h • KaehlerDifferential.map K K ↥(modularFunctionFieldC K N) ↥(charLDegeneracyRoof K N ℓ)
          (KaehlerDifferential.D K ↥(modularFunctionFieldC K N) (jGeomGen K N)))

def liftFun (hp5 : 5 ≤ p) (k : ℤ) (v : SSCarrier p N K hp5 k) : ↥(modularFunctionFieldC K N) :=
  Classical.epsilon (fun g : ↥(modularFunctionFieldC K N) =>
    (∀ z : Place K (modularFunctionFieldC K N), z ∈ ssPlaces p N K →
        -((ModularCurve.weightDivisor K N (k / 2).toNat) z) ≤ z.ord g) ∧
    (∀ x : SSIndex p N K hp5 k, lead N K x.1 (poleOrder p N K hp5 k x) g = v x))

def ssHeckeFun (hp5 : 5 ≤ p) (k : ℤ) (ℓ : ℕ) [NeZero ℓ] (v : SSCarrier p N K hp5 k) : SSCarrier p N K hp5 k :=
  fun x =>
    letI := AlgebraicCurve.algebraAlong (heckeAlphaC K N ℓ)
    algebraMap K K ((ℓ : K) ^ (k / 2 - 1)) *
      lead N K x.1 (poleOrder p N K hp5 k x)
        (Algebra.trace ↥(modularFunctionFieldC K N) ↥(charLDegeneracyRoof K N ℓ)
          (heckeBetaC K N ℓ (liftFun p N K hp5 k v) * heckeMultiplier N K ℓ ^ (k / 2).toNat))

def resQFun (hp5 : 5 ≤ p) (k : ℤ) (φ : PowerSeries K) : SSCarrier p N K hp5 k :=
  fun x =>
    lead N K x.1 (poleOrder p N K hp5 k x)
      (Classical.epsilon (fun G : ↥(modularFunctionFieldC K N) =>
        (G : LaurentSeries K) = HahnSeries.ofPowerSeries ℤ K φ * thetaL K (jqModC K) ^ (-(k / 2))))

end ModularCurve
end

Statements phrased using this module (36)