Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_HeckeOperatorTotal.lean

definition module

A total Hecke operator on Pic⁰ of modular function fields

Fix a field L with a \mathbb{Q}-algebra structure and positive integers N,\ell (encoded by NeZero). The ambient curve is the intermediate field L\cdot F_N := laurentBaseChange L (modularFunctionFieldFull N) inside \mathrm{LaurentSeries}\,L, i.e. the field generated over L by the coefficientwise image of \mathbb{Q}(q\text{-expansions } j(q^d) : d \mid N), and its group Pic0 of degree-zero divisor classes in the project's place-theoretic sense. Two L-algebra maps L\cdot F_N \to L\cdot F_{N\ell} are available: heckeAlphaBar, the inclusion coming from F_N \subseteq F_{N\ell}, and heckeBetaBar, induced by q \mapsto q^{\ell} (the Laurent-exponent dilation qExpand L ℓ).

The first definition, HeckeInputsAlong L N ℓ, is a single proposition bundling, as an iterated existential over proofs, exactly the five inputs needed to form the correspondence: integrality of the ring maps underlying heckeAlphaBar and heckeBetaBar; the property HasPrincipalDivisors at level N\ell; finiteness of L\cdot F_{N\ell} as a module over L\cdot F_N along heckeAlphaBar; and the conjunction of the fundamental identity \sum_{w\mid v} e_w \deg w = [F':F]\deg v along heckeBetaBar with the norm formula for divisor pushforward along heckeAlphaBar. Note that the finiteness witness is packed before the fundamental identity.

The second definition, heckeOperatorAlong L N ℓ, is a total closed term: an additive endomorphism of \mathrm{Pic}^0(L\cdot F_N) equal, by a case split on HeckeInputsAlong L N ℓ, to the correspondence \alpha_*\circ\beta^* (heckePic0Bar, pullback along heckeBetaBar followed by pushforward along heckeAlphaBar) when witnesses exist, and to the zero map otherwise. The three accompanying lemmas record the constructor for HeckeInputsAlong from the five inputs, the identification of heckeOperatorAlong with heckePic0Bar whenever the inputs are in hand, and the value 0 in the absence of inputs. Nothing is asserted about the inputs themselves, and no identification with the classical T_\ell or U_\ell action on q-expansions is made here.

Relation to Mathlib

Places, divisors, degree-zero classes, Pic0, pushforward/pullback and the fundamental identity used here are the project's own AlgebraicCurve development; Mathlib contributes the Laurent series, intermediate field and valuation-subring infrastructure, and has no notion of Hecke correspondence on a Jacobian.

Where it is used

This total term gives a single input-free symbol for the Hecke operator on the Jacobian of the modular curve of level N, so that statements about the Hecke action (in particular at L = \overline{\mathbb{Q}}, where the target is JZero N) can be formulated without carrying the five analytic and arithmetic inputs as binders. It serves the modular side of the argument, where Hecke eigenvalues on cuspidal classes and the Galois action on torsion of J_0(N) are compared.

References

  1. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Publications of the Mathematical Society of Japan 11, Princeton University Press, 1971, Chapters 3 and 7
  2. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §5.2 and §6.3
  3. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186

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

Imports

Imported by

Declarations

Source

import Definitions.Def_ModularCurve_HeckeOperator

set_option autoImplicit false

noncomputable section

namespace ModularCurve

open AlgebraicCurve

variable (L : Type*) [Field L] [Algebra ℚ L] (N ℓ : ℕ) [NeZero N] [NeZero ℓ]

def HeckeInputsAlong : Prop :=
  ∃ (_ : HeckeAlphaBarIntegral L N ℓ) (hβ : HeckeBetaBarIntegral L N ℓ)
    (_ : HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ))))
    (hfin : FiniteAlong L (heckeAlphaBar L N ℓ)),
    FundamentalIdentityAlong L (heckeBetaBar L N ℓ) hβ ∧
      NormFormulaAlong L (heckeAlphaBar L N ℓ) hfin

open Classical in

def heckeOperatorAlong :
    Pic0 L (laurentBaseChange L (modularFunctionFieldFull N)) →+
      Pic0 L (laurentBaseChange L (modularFunctionFieldFull N)) :=
  if h : HeckeInputsAlong L N ℓ then
    haveI := h.snd.snd.fst
    heckePic0Bar h.fst h.snd.fst h.snd.snd.snd.snd.1 h.snd.snd.snd.fst h.snd.snd.snd.snd.2
  else 0

variable {L N ℓ}

theorem heckeInputsAlong_intro (hα : HeckeAlphaBarIntegral L N ℓ) (hβ : HeckeBetaBarIntegral L N ℓ)
    [hP : HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))]
    (hFI : FundamentalIdentityAlong L (heckeBetaBar L N ℓ) hβ)
    (hfin : FiniteAlong L (heckeAlphaBar L N ℓ))
    (hN : NormFormulaAlong L (heckeAlphaBar L N ℓ) hfin) : HeckeInputsAlong L N ℓ :=
  ⟨hα, hβ, hP, hfin, hFI, hN⟩

theorem heckeOperatorAlong_eq (hα : HeckeAlphaBarIntegral L N ℓ) (hβ : HeckeBetaBarIntegral L N ℓ)
    [HasPrincipalDivisors L (laurentBaseChange L (modularFunctionFieldFull (N * ℓ)))]
    (hFI : FundamentalIdentityAlong L (heckeBetaBar L N ℓ) hβ)
    (hfin : FiniteAlong L (heckeAlphaBar L N ℓ))
    (hN : NormFormulaAlong L (heckeAlphaBar L N ℓ) hfin) :
    heckeOperatorAlong L N ℓ = heckePic0Bar hα hβ hFI hfin hN := by
  have h : HeckeInputsAlong L N ℓ := heckeInputsAlong_intro hα hβ hFI hfin hN
  rw [heckeOperatorAlong, dif_pos h]

theorem heckeOperatorAlong_of_not (h : ¬ HeckeInputsAlong L N ℓ) :
    heckeOperatorAlong L N ℓ = 0 := by
  rw [heckeOperatorAlong, dif_neg h]

end ModularCurve

end

Statements phrased using this module (6)