Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularForm_HeckeOperatorForms.lean

definition module

Hecke operators , on modular and cusp forms

For a weight k \in \mathbb{Z} and level \Gamma_0(N), this module packages the raw Hecke operators of ModularForm_HeckeOperator as bundled \mathbb{C}-linear endomorphisms of the Mathlib spaces ModularForm (CongruenceSubgroup.Gamma0 N) k and CuspForm (CongruenceSubgroup.Gamma0 N) k. Recall the underlying operators on functions f : \mathbb{H} \to \mathbb{C}: with \alpha_j = \begin{pmatrix}1 & j\\ 0 & p\end{pmatrix} and \delta_p = \begin{pmatrix}p & 0\\ 0 & 1\end{pmatrix} acting by the weight-k slash action, heckeU k p f = \sum_{j=0}^{p-1} f \mid_k \alpha_j, i.e. \tau \mapsto p^{-1}\sum_{j<p} f((\tau+j)/p), and heckeT k p f = heckeU k p f +\, f\mid_k \delta_p, i.e. the extra term p^{k-1}f(p\tau); on q-expansions these are the usual normalisations a_n \mapsto a_{np} and a_n \mapsto a_{np} + p^{k-1}a_{n/p}.

ModularForm.heckeTLin k hp hpN takes p prime and p \nmid N (whence N \neq 0, since p \mid 0) and sends f to the modular form whose underlying function is heckeT k p ⇑f; its three structure fields — \Gamma_0(N)-invariance under the weight-k slash action, holomorphy as a map of the upper half-plane, and boundedness at the cusps — are filled in by the imported theorems heckeT_slash_eq_self_of_mem_Gamma0, mdifferentiable_heckeT and ModularFormClass.isBoundedAt_heckeT. ModularForm.heckeULin k hpN does the same with heckeU under the hypotheses [NeZero N] and p \mid N; note that no primality of p is assumed for U_p. CuspForm.heckeTLin and CuspForm.heckeULin are the parallel constructions on cusp forms, with the boundedness field replaced by vanishing at the cusps via CuspFormClass.isZeroAt_heckeT/isZeroAt_heckeU. Additivity and \mathbb{C}-homogeneity come from heckeT_add, heckeT_smul, heckeU_add, heckeU_smul through injectivity of the coercion to functions. Four rfl lemmas (coe_heckeTLin_apply, coe_heckeULin_apply and their pointwise forms) record that the coercion of the bundled operator is the raw operator. Only T_p and U_p at a single prime are constructed here: no T_n for composite n, and no \Gamma_1(N) or nebentypus variants.

Relation to Mathlib

Built on Mathlib's ModularForm, CuspForm, CongruenceSubgroup.Gamma0 and weight-k slash action; Mathlib provides no Hecke operators on these spaces, so these linear endomorphisms are the project's own.

Where it is used

These bundled operators make the Hecke action on S_k(\Gamma_0(N)) expressible in Lean, and hence statements about commuting families, eigenforms and their eigenvalues — the input to the construction of the Galois representation attached to a weight-2 newform on \Gamma_0(N) used in the Frey curve argument.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §5.1–5.3
  2. G. Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, Princeton University Press, 1971, Ch. 3
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154, §1

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

Imports

Theorems imported by this definition module

Imported by

Declarations

Source

import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups ↗
import Definitions.Def_ModularForm_HeckeOperator
import Theorems.Thm_ModularForm_heckeT_slash_eq_self_of_mem_Gamma0
import Theorems.Thm_ModularForm_heckeU_slash_eq_self_of_mem_Gamma0
import Theorems.Thm_ModularForm_mdifferentiable_heckeT
import Theorems.Thm_ModularForm_mdifferentiable_heckeU
import Theorems.Thm_ModularFormClass_isBoundedAt_heckeT
import Theorems.Thm_ModularFormClass_isBoundedAt_heckeU
import Theorems.Thm_CuspFormClass_isZeroAt_heckeT
import Theorems.Thm_CuspFormClass_isZeroAt_heckeU

set_option autoImplicit false

noncomputable section

namespace ModularForm

variable {N : ℕ} {p : ℕ}

def heckeTLin (k : ℤ) (hp : p.Prime) (hpN : ¬ p ∣ N) :
    ModularForm (CongruenceSubgroup.Gamma0 N) k →ₗ[ℂ] ModularForm (CongruenceSubgroup.Gamma0 N) k :=
  haveI : NeZero N := ⟨fun h => hpN (h ▸ dvd_zero p)⟩
  { toFun := fun f =>
      { toFun := heckeT k p ⇑f
        slash_action_eq' := fun γ hγ => heckeT_slash_eq_self_of_mem_Gamma0 k hp hpN
          (fun γ hγ => SlashInvariantFormClass.slash_action_eq f γ hγ) γ hγ
        holo' := mdifferentiable_heckeT (ModularFormClass.holo f) k p
        bdd_at_cusps' := fun hc => ModularFormClass.isBoundedAt_heckeT f p hc }
    map_add' := fun f g => DFunLike.coe_injective <|
      show heckeT k p ⇑(f + g) = heckeT k p ⇑f + heckeT k p ⇑g by rw [ModularForm.coe_add, heckeT_add]
    map_smul' := fun c f => DFunLike.coe_injective <|
      show heckeT k p ⇑(c • f) = c • heckeT k p ⇑f by rw [ModularForm.IsGLPos.coe_smul, heckeT_smul] }

def heckeULin (k : ℤ) [NeZero N] (hpN : p ∣ N) :
    ModularForm (CongruenceSubgroup.Gamma0 N) k →ₗ[ℂ] ModularForm (CongruenceSubgroup.Gamma0 N) k where
  toFun f :=
    { toFun := heckeU k p ⇑f
      slash_action_eq' := fun γ hγ => heckeU_slash_eq_self_of_mem_Gamma0 k hpN
        (fun γ hγ => SlashInvariantFormClass.slash_action_eq f γ hγ) γ hγ
      holo' := mdifferentiable_heckeU (ModularFormClass.holo f) k p
      bdd_at_cusps' := fun hc => ModularFormClass.isBoundedAt_heckeU f p hc }
  map_add' f g := DFunLike.coe_injective <|
    show heckeU k p ⇑(f + g) = heckeU k p ⇑f + heckeU k p ⇑g by rw [ModularForm.coe_add, heckeU_add]
  map_smul' c f := DFunLike.coe_injective <|
    show heckeU k p ⇑(c • f) = c • heckeU k p ⇑f by rw [ModularForm.IsGLPos.coe_smul, heckeU_smul]

@[simp] theorem coe_heckeTLin_apply (k : ℤ) (hp : p.Prime) (hpN : ¬ p ∣ N)
    (f : ModularForm (CongruenceSubgroup.Gamma0 N) k) : ⇑(heckeTLin k hp hpN f) = heckeT k p ⇑f := rfl

@[simp] theorem coe_heckeULin_apply (k : ℤ) [NeZero N] (hpN : p ∣ N)
    (f : ModularForm (CongruenceSubgroup.Gamma0 N) k) : ⇑(heckeULin k hpN f) = heckeU k p ⇑f := rfl

theorem heckeTLin_apply_apply (k : ℤ) (hp : p.Prime) (hpN : ¬ p ∣ N)
    (f : ModularForm (CongruenceSubgroup.Gamma0 N) k) (τ : UpperHalfPlane) :
    heckeTLin k hp hpN f τ = heckeT k p ⇑f τ := rfl

theorem heckeULin_apply_apply (k : ℤ) [NeZero N] (hpN : p ∣ N)
    (f : ModularForm (CongruenceSubgroup.Gamma0 N) k) (τ : UpperHalfPlane) :
    heckeULin k hpN f τ = heckeU k p ⇑f τ := rfl

end ModularForm

namespace CuspForm

open ModularForm

variable {N : ℕ} {p : ℕ}

def heckeTLin (k : ℤ) (hp : p.Prime) (hpN : ¬ p ∣ N) :
    CuspForm (CongruenceSubgroup.Gamma0 N) k →ₗ[ℂ] CuspForm (CongruenceSubgroup.Gamma0 N) k :=
  haveI : NeZero N := ⟨fun h => hpN (h ▸ dvd_zero p)⟩
  { toFun := fun f =>
      { toFun := heckeT k p ⇑f
        slash_action_eq' := fun γ hγ => heckeT_slash_eq_self_of_mem_Gamma0 k hp hpN
          (fun γ hγ => SlashInvariantFormClass.slash_action_eq f γ hγ) γ hγ
        holo' := mdifferentiable_heckeT (CuspFormClass.holo f) k p
        zero_at_cusps' := fun hc => CuspFormClass.isZeroAt_heckeT f p hc }
    map_add' := fun f g => DFunLike.coe_injective <|
      show heckeT k p ⇑(f + g) = heckeT k p ⇑f + heckeT k p ⇑g by rw [CuspForm.coe_add, heckeT_add]
    map_smul' := fun c f => DFunLike.coe_injective <|
      show heckeT k p ⇑(c • f) = c • heckeT k p ⇑f by rw [CuspForm.IsGLPos.coe_smul, heckeT_smul] }

def heckeULin (k : ℤ) [NeZero N] (hpN : p ∣ N) :
    CuspForm (CongruenceSubgroup.Gamma0 N) k →ₗ[ℂ] CuspForm (CongruenceSubgroup.Gamma0 N) k where
  toFun f :=
    { toFun := heckeU k p ⇑f
      slash_action_eq' := fun γ hγ => heckeU_slash_eq_self_of_mem_Gamma0 k hpN
        (fun γ hγ => SlashInvariantFormClass.slash_action_eq f γ hγ) γ hγ
      holo' := mdifferentiable_heckeU (CuspFormClass.holo f) k p
      zero_at_cusps' := fun hc => CuspFormClass.isZeroAt_heckeU f p hc }
  map_add' f g := DFunLike.coe_injective <|
    show heckeU k p ⇑(f + g) = heckeU k p ⇑f + heckeU k p ⇑g by rw [CuspForm.coe_add, heckeU_add]
  map_smul' c f := DFunLike.coe_injective <|
    show heckeU k p ⇑(c • f) = c • heckeU k p ⇑f by rw [CuspForm.IsGLPos.coe_smul, heckeU_smul]

@[simp] theorem coe_heckeTLin_apply (k : ℤ) (hp : p.Prime) (hpN : ¬ p ∣ N)
    (f : CuspForm (CongruenceSubgroup.Gamma0 N) k) : ⇑(heckeTLin k hp hpN f) = heckeT k p ⇑f := rfl

@[simp] theorem coe_heckeULin_apply (k : ℤ) [NeZero N] (hpN : p ∣ N)
    (f : CuspForm (CongruenceSubgroup.Gamma0 N) k) : ⇑(heckeULin k hpN f) = heckeU k p ⇑f := rfl

theorem heckeTLin_apply_apply (k : ℤ) (hp : p.Prime) (hpN : ¬ p ∣ N)
    (f : CuspForm (CongruenceSubgroup.Gamma0 N) k) (τ : UpperHalfPlane) :
    heckeTLin k hp hpN f τ = heckeT k p ⇑f τ := rfl

theorem heckeULin_apply_apply (k : ℤ) [NeZero N] (hpN : p ∣ N)
    (f : CuspForm (CongruenceSubgroup.Gamma0 N) k) (τ : UpperHalfPlane) :
    heckeULin k hpN f τ = heckeU k p ⇑f τ := rfl

end CuspForm

end

Statements phrased using this module (64)