Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_HeckeAlgebra.lean

definition module

Hecke algebras acting on cusp forms for

For a level N with NeZero N, a weight k : \mathbb{Z} and an arbitrary set S \subseteq \mathbb{N} of "omitted" primes, CuspForm.heckeGenerators N k S is the subset of \operatorname{End}_{\mathbb{C}} S_k(\Gamma_0(N)) consisting of the operators heckeTLin k hℓ hℓN for primes \ell \nmid N with \ell \notin S, together with the operators heckeULin k hqN for primes q \mid N with q \notin S; here heckeTLin and heckeULin are the project's Hecke endomorphisms of the space of cusp forms, supplied by the imported module, and the membership predicate is literally an existential over such \ell, q with T equal to the corresponding operator. Then CuspForm.heckeAlgebra N k S is the \mathbb{Z}-subalgebra Algebra.adjoin ℤ of \operatorname{End}_{\mathbb{C}} S_k(\Gamma_0(N)) generated by that set. Thus S = \emptyset gives the full algebra generated by all T_\ell and U_q, while any S containing the primes dividing N gives an anemic algebra with no U_q generators; all choices of S live inside one ambient endomorphism ring.

The remaining declarations are bookkeeping around these two definitions: each generator lies in heckeGenerators and hence in heckeAlgebra; the generating set and the algebra are antitone in S (heckeGenerators_mono, heckeAlgebra_mono); any two generators commute, by case analysis on the four possible pairs using the imported commutation theorems heckeTLin_comm, heckeTLin_heckeULin_comm, heckeULin_comm. From this the module registers instances that the subalgebra is multiplicatively commutative, hence a CommRing, and that its additive group is torsion-free (proved from injectivity of scaling by a nonzero natural number on the ambient \mathbb{C}-module). Finally heckeAlgebra.T and heckeAlgebra.U package the generators as elements of the subalgebra, with rfl lemmas coe_T, coe_U identifying their images in \operatorname{End}_{\mathbb{C}} S_k(\Gamma_0(N)) with heckeTLin, heckeULin.

Relation to Mathlib

Mathlib supplies the space CuspForm (CongruenceSubgroup.Gamma0 N) k and the subalgebra machinery (Algebra.adjoin, Subalgebra), but the Hecke operators used as generators are the project's own endomorphisms from the imported module; the resulting Hecke algebra as a \mathbb{Z}-subalgebra of \operatorname{End}_{\mathbb{C}} of cusp forms is a project definition.

Where it is used

These commutative rings are the \mathbb{T} side of the modularity-lifting statements: the R = \mathbb{T} theorems are phrased with an anemic Hecke algebra \mathbb{T}^S (i.e. S containing the primes dividing the level) localised at a maximal ideal, and residual modularity is expressed by the existence of a maximal ideal of such an algebra containing p and the elements T_\ell - a_\ell. The CommRing and torsion-freeness instances are what allow ideals, residue fields, localisations and tensor products with \mathbb{Z}_p to be formed directly on the subalgebra.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005
  2. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

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

Imports

Theorems imported by this definition module

Imported by

Declarations

Source

import Definitions.Def_ModularForm_HeckeOperatorForms
import Theorems.Thm_CuspForm_heckeTLin_comm
import Theorems.Thm_CuspForm_heckeTLin_heckeULin_comm
import Theorems.Thm_CuspForm_heckeULin_comm

set_option autoImplicit false

noncomputable section

namespace CuspForm

variable (N : ℕ) [NeZero N] (k : ℤ) (S : Set ℕ)

def heckeGenerators : Set (Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) :=
  {T | ∃ (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N), ℓ ∉ S ∧ T = heckeTLin k hℓ hℓN} ∪
    {U | ∃ (q : ℕ) (hqN : q ∣ N), q.Prime ∧ q ∉ S ∧ U = heckeULin k hqN}

def heckeAlgebra : Subalgebra ℤ (Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) :=
  Algebra.adjoin ℤ (heckeGenerators N k S)

variable {N k S}

theorem heckeTLin_mem_heckeGenerators {ℓ : ℕ} (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N) (hℓS : ℓ ∉ S) :
    heckeTLin k hℓ hℓN ∈ heckeGenerators N k S :=
  Or.inl ⟨ℓ, hℓ, hℓN, hℓS, rfl⟩

theorem heckeULin_mem_heckeGenerators {q : ℕ} (hq : q.Prime) (hqN : q ∣ N) (hqS : q ∉ S) :
    heckeULin k hqN ∈ heckeGenerators N k S :=
  Or.inr ⟨q, hqN, hq, hqS, rfl⟩

theorem heckeTLin_mem_heckeAlgebra {ℓ : ℕ} (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N) (hℓS : ℓ ∉ S) :
    heckeTLin k hℓ hℓN ∈ heckeAlgebra N k S :=
  Algebra.subset_adjoin (heckeTLin_mem_heckeGenerators hℓ hℓN hℓS)

theorem heckeULin_mem_heckeAlgebra {q : ℕ} (hq : q.Prime) (hqN : q ∣ N) (hqS : q ∉ S) :
    heckeULin k hqN ∈ heckeAlgebra N k S :=
  Algebra.subset_adjoin (heckeULin_mem_heckeGenerators hq hqN hqS)

theorem heckeGenerators_mono {S S' : Set ℕ} (h : S ⊆ S') :
    heckeGenerators N k S' ⊆ heckeGenerators N k S := by
  rintro T (⟨ℓ, hℓ, hℓN, hℓS, rfl⟩ | ⟨q, hqN, hq, hqS, rfl⟩)
  · exact heckeTLin_mem_heckeGenerators hℓ hℓN fun hS => hℓS (h hS)
  · exact heckeULin_mem_heckeGenerators hq hqN fun hS => hqS (h hS)

theorem heckeAlgebra_mono {S S' : Set ℕ} (h : S ⊆ S') : heckeAlgebra N k S' ≤ heckeAlgebra N k S :=
  Algebra.adjoin_mono (heckeGenerators_mono h)

theorem commute_of_mem_heckeGenerators {T T' : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)}
    (hT : T ∈ heckeGenerators N k S) (hT' : T' ∈ heckeGenerators N k S) : Commute T T' := by
  rcases hT with ⟨ℓ, hℓ, hℓN, -, rfl⟩ | ⟨q, hqN, -, -, rfl⟩ <;>
    rcases hT' with ⟨ℓ', hℓ', hℓ'N, -, rfl⟩ | ⟨q', hq'N, -, -, rfl⟩
  · exact heckeTLin_comm k hℓ hℓN hℓ' hℓ'N
  · exact heckeTLin_heckeULin_comm k hℓ hℓN hq'N
  · exact (heckeTLin_heckeULin_comm k hℓ' hℓ'N hqN).symm
  · exact heckeULin_comm k hqN hq'N

variable (N k S)

instance heckeAlgebra.instIsMulCommutative : IsMulCommutative (heckeAlgebra N k S) :=
  Algebra.isMulCommutative_adjoin ℤ fun _ hT _ hT' => commute_of_mem_heckeGenerators hT hT'

open scoped IsMulCommutative in

instance heckeAlgebra.instCommRing : CommRing (heckeAlgebra N k S) := inferInstance

instance heckeAlgebra.instIsAddTorsionFree : IsAddTorsionFree (heckeAlgebra N k S) where
  nsmul_right_injective n hn a b hab := by
    apply Subtype.ext
    have h : (n : ℂ) • (a : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) =
        (n : ℂ) • (b : Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) := by
      simp only [Nat.cast_smul_eq_nsmul]
      exact congrArg Subtype.val hab
    exact smul_right_injective _ (Nat.cast_ne_zero.mpr hn) h

variable {N k S}

def heckeAlgebra.T {ℓ : ℕ} (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N) (hℓS : ℓ ∉ S) : heckeAlgebra N k S :=
  ⟨heckeTLin k hℓ hℓN, heckeTLin_mem_heckeAlgebra hℓ hℓN hℓS⟩

def heckeAlgebra.U {q : ℕ} (hq : q.Prime) (hqN : q ∣ N) (hqS : q ∉ S) : heckeAlgebra N k S :=
  ⟨heckeULin k hqN, heckeULin_mem_heckeAlgebra hq hqN hqS⟩

@[simp] theorem heckeAlgebra.coe_T {ℓ : ℕ} (hℓ : ℓ.Prime) (hℓN : ¬ ℓ ∣ N) (hℓS : ℓ ∉ S) :
    ((heckeAlgebra.T hℓ hℓN hℓS : heckeAlgebra N k S) :
      Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) = heckeTLin k hℓ hℓN := rfl

@[simp] theorem heckeAlgebra.coe_U {q : ℕ} (hq : q.Prime) (hqN : q ∣ N) (hqS : q ∉ S) :
    ((heckeAlgebra.U hq hqN hqS : heckeAlgebra N k S) :
      Module.End ℂ (CuspForm (CongruenceSubgroup.Gamma0 N) k)) = heckeULin k hqN := rfl

end CuspForm

end

Statements phrased using this module (148)