Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_CuspForm_HeckeWord.lean

definition module

Hecke words: free-algebra evaluation of Hecke operators

Fix a level N, a weight k \in \mathbb{Z} and a set S \subseteq \mathbb{N} of excluded indices. A "Hecke word" is an element of the free associative \mathbb{Z}-algebra FreeAlgebra ℤ ℕ on the naturals, i.e. a noncommutative integral polynomial in formal symbols indexed by n \in \mathbb{N}; the module sets up two evaluations of such words.

On the complex vector space S_k(\Gamma_0(N)) of cusp forms, CuspForm.heckeWordGenForms sends n to 0 unless n is prime and n \notin S, in which case it sends n to heckeULin at n if n \mid N and to heckeTLin at n otherwise; here heckeTLin, heckeULin are the endomorphisms induced by f \mapsto \sum_{j<p} f \mid_k \begin{pmatrix}1&j\\0&p\end{pmatrix} and its sum with f \mid_k \begin{pmatrix}p&0\\0&1\end{pmatrix}. Three lemmas record the three branches. CuspForm.heckeWordForms is the induced \mathbb{Z}-algebra homomorphism FreeAlgebra ℤ ℕ → Module.End ℂ (CuspForm (Gamma0 N) k), with heckeWordForms_ι computing it on generators. range_heckeWordForms identifies its image with heckeAlgebra N k S, the \mathbb{Z}-subalgebra generated by the T_\ell (\ell prime, \ell \nmid N, \ell \notin S) and the U_q (q prime, q \mid N, q \notin S); the two corollaries state that every element of that algebra is the value of some Hecke word, and conversely that all such values lie in it.

In the HeckeEis namespace the same recipe is applied to \mathbb{Z}-linear endomorphisms of \mathrm{Hom}(\Gamma_0(N)^{\mathrm{add}}, A) for an additive abelian group A: heckeWordGenHom sends a prime n \notin S to the transfer operator heckeOperatorHom N n A, the composite of pullback along the conjugation map \gamma \mapsto \alpha^{-1}\gamma\alpha, \alpha = \mathrm{diag}(1,n), defined on the subgroup of \gamma \in \Gamma_0(N) with n dividing the upper right entry, with the corestriction (transfer) back to \Gamma_0(N), and sends all other n to 0. A single corestriction recipe thus covers both n \nmid N and n \mid N. heckeWordHom is the resulting algebra homomorphism from FreeAlgebra ℤ ℕ, together with its values on generators.

Relation to Mathlib

The evaluations are Mathlib's FreeAlgebra.lift and the target algebras are Mathlib's endomorphism algebras; the Hecke operators heckeTLin, heckeULin, heckeOperatorHom and the subalgebra heckeAlgebra being evaluated into are the project's own definitions.

Where it is used

Using the free algebra on \mathbb{N} as the source means one element can be evaluated simultaneously on cusp forms and on additive characters of \Gamma_0(N), with no commutation relations between the operators built into the definitions; this is how the Hecke action is transported between the analytic model and the group-theoretic (transfer) model. The cusp-form side yields in particular that the Hecke algebra generated by the T_\ell and U_q away from S is exactly the set of values of Hecke words.

References

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

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

Imports

Imported by

  • no other definition module

Declarations

Source

import Mathlib.Algebra.FreeAlgebra ↗
import Definitions.Def_CuspForm_HeckeAlgebra
import Definitions.Def_Gamma0HeckeOperatorHom

open CongruenceSubgroup

namespace CuspForm

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

noncomputable def heckeWordGenForms (n : ℕ) : Module.End ℂ (CuspForm (Gamma0 N) k) :=
  if h : n.Prime ∧ n ∉ S then
    (if hn : n ∣ N then heckeULin k hn else heckeTLin k h.1 hn)
  else 0

variable {N k S} in
theorem heckeWordGenForms_of_not_dvd {n : ℕ} (hn : n.Prime) (hnN : ¬ n ∣ N) (hnS : n ∉ S) :
    heckeWordGenForms N k S n = heckeTLin k hn hnN := by
  rw [heckeWordGenForms, dif_pos ⟨hn, hnS⟩, dif_neg hnN]

variable {N k S} in
theorem heckeWordGenForms_of_dvd {n : ℕ} (hn : n.Prime) (hnN : n ∣ N) (hnS : n ∉ S) :
    heckeWordGenForms N k S n = heckeULin k hnN := by
  rw [heckeWordGenForms, dif_pos ⟨hn, hnS⟩, dif_pos hnN]

variable {N k S} in
theorem heckeWordGenForms_of_not {n : ℕ} (h : ¬ (n.Prime ∧ n ∉ S)) : heckeWordGenForms N k S n = 0 := by
  rw [heckeWordGenForms, dif_neg h]

noncomputable def heckeWordForms : FreeAlgebra ℤ ℕ →ₐ[ℤ] Module.End ℂ (CuspForm (Gamma0 N) k) :=
  FreeAlgebra.lift ℤ (heckeWordGenForms N k S)

@[simp] theorem heckeWordForms_ι (n : ℕ) :
    heckeWordForms N k S (FreeAlgebra.ι ℤ n) = heckeWordGenForms N k S n :=
  FreeAlgebra.lift_ι_apply _ _

theorem range_heckeWordForms : (heckeWordForms N k S).range = heckeAlgebra N k S := by
  rw [heckeWordForms, ← Algebra.adjoin_range_eq_range_freeAlgebra_lift, heckeAlgebra]
  apply le_antisymm
  · refine Algebra.adjoin_le ?_
    rintro _ ⟨n, rfl⟩
    by_cases h : n.Prime ∧ n ∉ S
    · by_cases hn : n ∣ N
      · rw [heckeWordGenForms_of_dvd h.1 hn h.2]
        exact Algebra.subset_adjoin (heckeULin_mem_heckeGenerators h.1 hn h.2)
      · rw [heckeWordGenForms_of_not_dvd h.1 hn h.2]
        exact Algebra.subset_adjoin (heckeTLin_mem_heckeGenerators h.1 hn h.2)
    · rw [heckeWordGenForms_of_not h]
      exact Subalgebra.zero_mem _
  · refine Algebra.adjoin_mono ?_
    rintro T hT
    rcases hT with ⟨ℓ, hℓ, hℓN, hℓS, rfl⟩ | ⟨q, hqN, hq, hqS, rfl⟩
    · exact ⟨ℓ, heckeWordGenForms_of_not_dvd hℓ hℓN hℓS⟩
    · exact ⟨q, heckeWordGenForms_of_dvd hq hqN hqS⟩

theorem exists_heckeWordForms_eq (t : heckeAlgebra N k S) :
    ∃ P : FreeAlgebra ℤ ℕ, heckeWordForms N k S P = t := by
  have h : (t : Module.End ℂ (CuspForm (Gamma0 N) k)) ∈ (heckeWordForms N k S).range := by
    rw [range_heckeWordForms]
    exact t.2
  exact h

theorem heckeWordForms_mem (P : FreeAlgebra ℤ ℕ) : heckeWordForms N k S P ∈ heckeAlgebra N k S := by
  rw [← range_heckeWordForms]
  exact ⟨P, rfl⟩

end CuspForm

namespace HeckeEis

variable (N : ℕ) (A : Type*) [AddCommGroup A] (S : Set ℕ) [DecidablePred (· ∈ S)]

noncomputable def heckeWordGenHom (n : ℕ) : Module.End ℤ (Additive (Gamma0 N) →+ A) :=
  if h : n.Prime ∧ n ∉ S then
    (haveI : NeZero n := ⟨h.1.ne_zero⟩; (heckeOperatorHom N n A).toIntLinearMap)
  else 0

variable {N A S} in
theorem heckeWordGenHom_of_prime {n : ℕ} (hn : n.Prime) (hnS : n ∉ S) :
    heckeWordGenHom N A S n
      = (haveI : NeZero n := ⟨hn.ne_zero⟩; (heckeOperatorHom N n A).toIntLinearMap) := by
  rw [heckeWordGenHom, dif_pos ⟨hn, hnS⟩]

variable {N A S} in
theorem heckeWordGenHom_of_not {n : ℕ} (h : ¬ (n.Prime ∧ n ∉ S)) : heckeWordGenHom N A S n = 0 := by
  rw [heckeWordGenHom, dif_neg h]

noncomputable def heckeWordHom : FreeAlgebra ℤ ℕ →ₐ[ℤ] Module.End ℤ (Additive (Gamma0 N) →+ A) :=
  FreeAlgebra.lift ℤ (heckeWordGenHom N A S)

@[simp] theorem heckeWordHom_ι (n : ℕ) :
    heckeWordHom N A S (FreeAlgebra.ι ℤ n) = heckeWordGenHom N A S n :=
  FreeAlgebra.lift_ι_apply _ _

variable {N A S} in
theorem heckeWordHom_ι_apply_of_prime {n : ℕ} (hn : n.Prime) (hnS : n ∉ S)
    (φ : Additive (Gamma0 N) →+ A) :
    heckeWordHom N A S (FreeAlgebra.ι ℤ n) φ
      = (haveI : NeZero n := ⟨hn.ne_zero⟩; heckeOperatorHom N n A φ) := by
  rw [heckeWordHom_ι, heckeWordGenHom_of_prime hn hnS]
  rfl

end HeckeEis

Statements phrased using this module (1)