Hecke operators T_n on modular forms

For a positive integer n, the classical Hecke operator T_n at level Γ₁(N) is the slash operator attached to the double coset

Γ₁(N) · diag(1, n) · Γ₁(N).

The double coset and its slash operator already exist as diagCosetGamma1 N n and heckeSlashGamma1ModularFormEnd; this file packages their composite under the uniform name heckeTNat. The cusp-form operator heckeTCuspNat uses the same double coset, so preservation of cuspidality is inherited from the general slash construction rather than reproved.

The computation rules identify T_p at a prime with the single good-and-bad-prime formula from HeckeSlash/Prime.lean. When p ∣ N, they identify it with the upper-triangular operator, the operator modern sources call U_p. Thus the normalization is fixed by the abstract double coset before the multiplicativity and prime-power recurrences are developed.

Main definitions

• HeckeRing.GL2.heckeTNat: T_n on M_k(Γ₁(N)).
• HeckeRing.GL2.heckeTCuspNat: T_n on S_k(Γ₁(N)).

Main results

• HeckeRing.GL2.coe_heckeTNat, HeckeRing.GL2.coe_heckeTCuspNat: the underlying slash sums.
• HeckeRing.GL2.heckeTNat_coe_cuspForm: T_n agrees under the coercion from cusp forms to modular forms.
• HeckeRing.GL2.heckeTCuspNat_eq_smul_iff_heckeTNat_eq_smul: transfer an eigen-relation between a cusp form and its underlying modular form.
• HeckeRing.GL2.heckeTNat_congr, HeckeRing.GL2.heckeTCuspNat_congr: transport the index across an equality despite its NeZero instance argument.
• HeckeRing.GL2.heckeTNat_one, HeckeRing.GL2.heckeTCuspNat_one: T₁ is the identity.
• HeckeRing.GL2.coe_heckeTNat_prime, HeckeRing.GL2.coe_heckeTCuspNat_prime: the classical formula for T_p at every prime.
• HeckeRing.GL2.heckeTNat_eq_upperTri, HeckeRing.GL2.heckeTCuspNat_eq_upperTri: at a prime dividing the level, T_p is the upper-triangular operator.

Provenance

The definition follows heckeT_n in the AINTLIB LeanModularForms project (HeckeRIngs/GL2/HeckeT_n.lean, Chris Birkbeck, Apache-2.0, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08). That source assembles prime-power operators first; here the already-constructed double-coset action gives the equivalent canonical definition directly. No proof code is transcribed.

References

• F. Diamond and J. Shurman, A first course in modular forms, Propositions 5.2.1--5.2.2 and §5.3.
• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5.

noncomputable def HeckeRing.GL2.heckeTNat {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [_hn : NeZero n] : Module.End ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The Hecke operator T_n on M_k(Γ₁(N)). It is the slash operator of the canonical double coset Γ₁(N) · diag(1, n) · Γ₁(N).

The NeZero n binder records the classical convention that Hecke operators are indexed by positive integers, and it is not optional: at n = 0 the entry tuple ![1, 0] fails the positivity side condition of natDiagGL, which then returns its junk value 1, so the double coset degenerates to Γ₁(N) itself and the construction would silently be the identity operator rather than T₀. The binder is _-named because only the statements below use it — the body is the same slash operator either way, and it is the index that is being constrained.

Equations

• HeckeRing.GL2.heckeTNat k n = HeckeRing.GL2.heckeSlashGamma1ModularFormEnd k (HeckeRing.GL2.diagCosetGamma1 N n)

noncomputable def HeckeRing.GL2.heckeTCuspNat {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [_hn : NeZero n] : Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The Hecke operator T_n on S_k(Γ₁(N)). This is the cusp-form operator attached to the same double coset as heckeTNat; in particular, it records that T_n preserves cuspidality. The index is nonzero for the reason explained on heckeTNat.

Equations

• HeckeRing.GL2.heckeTCuspNat k n = HeckeRing.GL2.heckeSlashGamma1CuspFormEnd k (HeckeRing.GL2.diagCosetGamma1 N n)

theorem HeckeRing.GL2.heckeTNat_def {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] : heckeTNat k n = heckeSlashGamma1ModularFormEnd k (diagCosetGamma1 N n)

The defining equation of heckeTNat.

theorem HeckeRing.GL2.heckeTCuspNat_def {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] : heckeTCuspNat k n = heckeSlashGamma1CuspFormEnd k (diagCosetGamma1 N n)

The defining equation of heckeTCuspNat.

theorem HeckeRing.GL2.heckeTNat_congr {N : ℕ} [NeZero N] (k : ℤ) {n m : ℕ} [NeZero n] [NeZero m] (h : n = m) : heckeTNat k n = heckeTNat k m

Transport T_n along an equality of indices. The NeZero side condition is a Prop, so the two operators are the same object; the lemma exists because rewriting the index inside heckeTNat would leave the instance argument stranded at the old index.

theorem HeckeRing.GL2.heckeTCuspNat_congr {N : ℕ} [NeZero N] (k : ℤ) {n m : ℕ} [NeZero n] [NeZero m] (h : n = m) : heckeTCuspNat k n = heckeTCuspNat k m

Transport the cusp-form T_n along an equality of indices.

@[simp]

theorem HeckeRing.GL2.coe_heckeTNat {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeTNat k n) f) = heckeSlashSum k (diagCosetGamma1 N n) ⇑f

On underlying functions, T_n is the slash sum of its defining double coset.

@[simp]

theorem HeckeRing.GL2.coe_heckeTCuspNat {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeTCuspNat k n) f) = heckeSlashSum k (diagCosetGamma1 N n) ⇑f

On underlying functions, the cusp-form T_n is the same slash sum.

@[simp]

theorem HeckeRing.GL2.heckeTNat_coe_cuspForm {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : (heckeTNat k n) (ModularFormClass.modularForm f) = ModularFormClass.modularForm ((heckeTCuspNat k n) f)

The modular-form and cusp-form T_n operators agree under the coercion S_k(Γ₁(N)) → M_k(Γ₁(N)).

theorem HeckeRing.GL2.heckeTCuspNat_eq_smul_iff_heckeTNat_eq_smul {N : ℕ} [NeZero N] (k : ℤ) (n : ℕ) [NeZero n] (F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (c : ℂ) : (heckeTCuspNat k n) F = c • F ↔ (heckeTNat k n) (ModularFormClass.modularForm F) = c • ModularFormClass.modularForm F

A cusp form satisfies a T_n eigen-relation exactly when its underlying modular form does. The two operators are defined by the same slash sum.

theorem HeckeRing.GL2.coe_heckeTNat_prime {N p : ℕ} [NeZero N] (k : ℤ) (hp : Nat.Prime p) (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeTNat k p) f) = heckeSlashUpperTri k p ⇑f + SlashAction.map k (scaleRep p) ⇑((diamondOpNat k p) f)

The classical T_p formula on modular forms, at every prime.

theorem HeckeRing.GL2.coe_heckeTCuspNat_prime {N p : ℕ} [NeZero N] (k : ℤ) (hp : Nat.Prime p) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) : ⇑((heckeTCuspNat k p) f) = heckeSlashUpperTri k p ⇑f + SlashAction.map k (scaleRep p) ⇑((diamondOpCuspNat k p) f)

The classical T_p formula on cusp forms, at every prime.

theorem HeckeRing.GL2.heckeTNat_eq_upperTri {N p : ℕ} [NeZero N] (k : ℤ) (hpN : p ∣ N) : heckeTNat k p = heckeSlashUpperTriModularFormEnd k hpN

At a positive index dividing the level, T_p is the upper-triangular operator. This is the operator modern sources denote by U_p.

theorem HeckeRing.GL2.heckeTCuspNat_eq_upperTri {N p : ℕ} [NeZero N] (k : ℤ) (hpN : p ∣ N) : heckeTCuspNat k p = heckeSlashUpperTriCuspFormEnd k hpN

At a positive index dividing the level, the cusp-form T_p is the upper-triangular operator.

@[simp]

theorem HeckeRing.GL2.heckeTNat_one {N : ℕ} [NeZero N] (k : ℤ) : heckeTNat k 1 = 1

The first Hecke operator on modular forms is the identity.

@[simp]

theorem HeckeRing.GL2.heckeTCuspNat_one {N : ℕ} [NeZero N] (k : ℤ) : heckeTCuspNat k 1 = 1

The first Hecke operator on cusp forms is the identity.