The Hecke operators Tₙ at level one

For a positive integer n, the classical Hecke operator Tₙ on modular forms of weight k on SL(2, ℤ) sums the slashes of f over a set of representatives of SL(2, ℤ) \ ℳₙ, where ℳₙ is the set of integral matrices of determinant n. With the upper-triangular representatives (a b; 0 d), ad = n, 0 < a, 0 ≤ b < d, of FixedDetMatrices.reps n, this is

Tₙ f = ∑_{(a b; 0 d)} f ∣[k] (a b; 0 d),

which, with Mathlib's normalization of the slash action, is (Tₙ f)(τ) = n^(k-1) ∑_{ad = n} ∑_{0 ≤ b < d} d^(-k) f((aτ + b)/d).

Unlike the operator HeckeRing.GL2.heckeTNat of the single double coset SL(2, ℤ) diag(1, n) SL(2, ℤ), the sum runs over all of ℳₙ, that is over every double coset SL(2, ℤ) diag(a, d) SL(2, ℤ) with a ∣ d and ad = n; so it is the classical Tₙ at every n, not only at squarefree ones. The representatives are those through which Popa and Zagier compute the Hecke action on period polynomials.

On q-expansions, Tₙ has the classical divisor-sum formula

aₘ(Tₙ f) = ∑_{d ∣ (m, n)} d^(k-1) a_{mn/d²}(f),

for every m ≥ 0, which is the arithmetic normalization of the Hecke operators fixed by Diamond–Shurman. It is computed from the factorization (a b; 0 d) = (1 b; 0 d) · diag(a, 1) of the representatives. The d representatives with the same diagonal (a, d) sum to (U_d f) ∣[k] diag(a, 1), where U_d f = ∑_{b < d} f ∣[k] (1 b; 0 d) has coefficients aₘ(U_d f) = a_{dm}(f), and slashing by diag(a, 1) spreads an expansion along a ℕ and multiplies it by a^(k-1). Summing over the factor pairs ad = n gives the formula. In particular a₁(Tₙ f) = aₙ(f) and a₀(Tₙ f) = (∑_{d ∣ n} d^(k-1)) a₀(f). The formula has the shape of the level-N formula HeckeRing.GL2.qExpansion_coeff_heckeRingHomCharSpace_heckeTCompositeGamma0_of_ne_zero for the Hecke-ring element HeckeRing.GL2.heckeTCompositeGamma0 N n, with trivial character; no comparison of the two operators is made here.

The sum is independent of the representatives in the sense that matters here: right multiplication by γ ∈ SL(2, ℤ) permutes the cosets SL(2, ℤ) A, so Tₙ f is invariant under SL(2, ℤ) when f is (TauCeti.heckeSlashLevelOne_slash_eq). Holomorphy and the behaviour at the cusps pass through finite sums of rational slashes, so Tₙ preserves modular and cusp forms.

Main definitions

• TauCeti.heckeSlashLevelOne k n f: the slash sum ∑ f ∣[k] (a b; 0 d) over the representatives FixedDetMatrices.reps n, for a function f : ℍ → ℂ.
• TauCeti.heckeTLevelOne k n: Tₙ on M_k(SL(2, ℤ)).
• TauCeti.heckeTCuspLevelOne k n: Tₙ on S_k(SL(2, ℤ)).

Main results

• TauCeti.heckeSlashLevelOne_slash_eq: the slash sum of an SL(2, ℤ)-invariant function is SL(2, ℤ)-invariant.
• TauCeti.mdifferentiable_heckeSlashLevelOne: the slash sum of a holomorphic function is holomorphic.
• TauCeti.coe_heckeTLevelOne, TauCeti.coe_heckeTCuspLevelOne: both operators are the slash sum on underlying functions, and TauCeti.heckeTLevelOne_coe_cuspForm: they agree on cusp forms.
• TauCeti.heckeSlashLevelOne_eq_sum_heckeSlashUpperTri_slash: the slash sum is ∑_{ad = n} (U_d f) ∣[k] diag(a, 1).
• TauCeti.hasSum_qExpansion_heckeSlashLevelOne: the q-expansion of the slash sum of a 1-periodic holomorphic function bounded at i∞.
• TauCeti.qExpansion_coeff_heckeTLevelOne, TauCeti.qExpansion_coeff_heckeTCuspLevelOne: the coefficient formula aₘ(Tₙ f) = ∑_{d ∣ (m, n)} d^(k-1) a_{mn/d²}(f).
• TauCeti.qExpansion_coeff_one_heckeTLevelOne, TauCeti.qExpansion_coeff_one_heckeTCuspLevelOne: a₁(Tₙ f) = aₙ(f); TauCeti.qExpansion_coeff_zero_heckeTLevelOne: a₀(Tₙ f) = (∑_{d ∣ n} d^(k-1)) a₀(f).

References

• J.-P. Serre, A course in arithmetic, Chapter VII, §5.
• F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.3.1.
• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327, §2.

noncomputable def TauCeti.heckeSlashLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

The level-one Hecke slash sum ∑ f ∣[k] (a b; 0 d), over the upper-triangular representatives (a b; 0 d) of SL(2, ℤ) \ ℳₙ in FixedDetMatrices.reps n. On a level-one modular form this is the classical Hecke operator Tₙ (TauCeti.heckeTLevelOne).

theorem TauCeti.heckeSlashLevelOne_def (k : ℤ) (n : ℕ) [NeZero n] (f : UpperHalfPlane → ℂ) : heckeSlashLevelOne k n f = ∑ A : ↑(FixedDetMatrices.reps ↑n), SlashAction.map k (FixedDetMatrices.toGL ⋯ ↑A) f

The defining equation of heckeSlashLevelOne.

@[simp]

theorem TauCeti.heckeSlashLevelOne_add (k : ℤ) (n : ℕ) [NeZero n] (f g : UpperHalfPlane → ℂ) : heckeSlashLevelOne k n (f + g) = heckeSlashLevelOne k n f + heckeSlashLevelOne k n g

The slash sum is additive in f.

@[simp]

theorem TauCeti.heckeSlashLevelOne_smul (k : ℤ) (n : ℕ) [NeZero n] (c : ℂ) (f : UpperHalfPlane → ℂ) : heckeSlashLevelOne k n (c • f) = c • heckeSlashLevelOne k n f

The slash sum is homogeneous in f: every representative has positive determinant n, so scalars pass through the slashes.

Invariance under SL(2, ℤ)

theorem TauCeti.heckeSlashLevelOne_slash_eq (k : ℤ) (n : ℕ) [NeZero n] {f : UpperHalfPlane → ℂ} (hf : ∀ γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range, SlashAction.map k γ f = f) {γ : GL (Fin 2) ℝ} (hγ : γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range) : SlashAction.map k γ (heckeSlashLevelOne k n f) = heckeSlashLevelOne k n f

The slash sum of an SL(2, ℤ)-invariant function is SL(2, ℤ)-invariant. Right multiplication by γ ∈ SL(2, ℤ) permutes the cosets SL(2, ℤ) A, A ∈ ℳₙ, and the slash of an invariant function by A depends only on the coset of A.

The operators on modular forms and cusp forms

theorem TauCeti.mdifferentiable_heckeSlashLevelOne (k : ℤ) (n : ℕ) [NeZero n] {f : UpperHalfPlane → ℂ} (hf : MDiff f) : MDiff (heckeSlashLevelOne k n f)

The slash sum of a holomorphic function is holomorphic.

noncomputable def TauCeti.heckeTLevelOne (k : ℤ) (n : ℕ) [NeZero n] : Module.End ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)

The Hecke operator Tₙ on M_k(SL(2, ℤ)), f ↦ ∑ f ∣[k] (a b; 0 d), the sum over the upper-triangular representatives of SL(2, ℤ) \ ℳₙ. It runs over all of ℳₙ, so it is the classical Tₙ at every n ≥ 1.

noncomputable def TauCeti.heckeTCuspLevelOne (k : ℤ) (n : ℕ) [NeZero n] : Module.End ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)

The Hecke operator Tₙ on S_k(SL(2, ℤ)): the operator heckeTLevelOne restricted to cusp forms, which it preserves.

@[simp]

theorem TauCeti.coe_heckeTLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ⇑((heckeTLevelOne k n) f) = heckeSlashLevelOne k n ⇑f

On underlying functions, Tₙ is the slash sum over the representatives of SL(2, ℤ) \ ℳₙ.

@[simp]

theorem TauCeti.coe_heckeTCuspLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ⇑((heckeTCuspLevelOne k n) f) = heckeSlashLevelOne k n ⇑f

On underlying functions, the cusp-form Tₙ is the slash sum over the representatives of SL(2, ℤ) \ ℳₙ.

theorem TauCeti.heckeTLevelOne_coe_cuspForm (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : (heckeTLevelOne k n) (ModularFormClass.modularForm f) = ModularFormClass.modularForm ((heckeTCuspLevelOne k n) f)

Tₙ commutes with the inclusion of cusp forms into modular forms.

Fourier coefficients

theorem TauCeti.heckeSlashLevelOne_eq_sum_heckeSlashUpperTri_slash (k : ℤ) (n : ℕ) [NeZero n] (f : UpperHalfPlane → ℂ) : heckeSlashLevelOne k n f = ∑ p ∈ n.divisorsAntidiagonal, SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![p.1, 1]) (HeckeRing.GL2.heckeSlashUpperTri k p.2 f)

The slash sum by diagonal type: ∑ f ∣[k] (a b; 0 d) = ∑_{ad = n} (U_d f) ∣[k] diag(a, 1), where U_d f = ∑_{b < d} f ∣[k] (1 b; 0 d) is HeckeRing.GL2.heckeSlashUpperTri k d f.

theorem TauCeti.hasSum_qExpansion_heckeSlashLevelOne (k : ℤ) (n : ℕ) [NeZero n] {f : UpperHalfPlane → ℂ} (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (hfhol : MDiff f) (hfbdd : UpperHalfPlane.IsBoundedAtImInfty f) (τ : UpperHalfPlane) : HasSum (fun (m : ℕ) => (∑ d ∈ (m.gcd n).divisors, ↑d ^ (k - 1) * (PowerSeries.coeff (m * n / d ^ 2)) (UpperHalfPlane.qExpansion 1 f)) • Function.Periodic.qParam 1 ↑τ ^ m) (heckeSlashLevelOne k n f τ)

The q-expansion of the level-one Hecke slash sum. For a 1-periodic holomorphic f bounded at i∞, the slash sum ∑ f ∣[k] (a b; 0 d) has the expansion ∑ₘ (∑_{d ∣ (m, n)} d^(k-1) a_{mn/d²}(f)) qᵐ at every point.

theorem TauCeti.qExpansion_coeff_heckeTLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeTLevelOne k n) f)) = ∑ d ∈ (m.gcd n).divisors, ↑d ^ (k - 1) * (PowerSeries.coeff (m * n / d ^ 2)) (UpperHalfPlane.qExpansion 1 ⇑f)

The coefficient formula for Tₙ on M_k(SL(2, ℤ)): aₘ(Tₙ f) = ∑_{d ∣ (m, n)} d^(k-1) a_{mn/d²}(f) for every m.

theorem TauCeti.qExpansion_coeff_heckeTCuspLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑((heckeTCuspLevelOne k n) f)) = ∑ d ∈ (m.gcd n).divisors, ↑d ^ (k - 1) * (PowerSeries.coeff (m * n / d ^ 2)) (UpperHalfPlane.qExpansion 1 ⇑f)

The coefficient formula for Tₙ on S_k(SL(2, ℤ)): aₘ(Tₙ f) = ∑_{d ∣ (m, n)} d^(k-1) a_{mn/d²}(f) for every m.

theorem TauCeti.qExpansion_coeff_one_heckeTLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((heckeTLevelOne k n) f)) = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f)

The first coefficient of Tₙ f is the n-th coefficient of f: a₁(Tₙ f) = aₙ(f).

theorem TauCeti.qExpansion_coeff_one_heckeTCuspLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑((heckeTCuspLevelOne k n) f)) = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f)

The first coefficient of Tₙ f is the n-th coefficient of f: a₁(Tₙ f) = aₙ(f).

theorem TauCeti.qExpansion_coeff_zero_heckeTLevelOne (k : ℤ) (n : ℕ) [NeZero n] (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑((heckeTLevelOne k n) f)) = (∑ d ∈ n.divisors, ↑d ^ (k - 1)) * (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑f)

The constant coefficient of Tₙ f is a₀(Tₙ f) = (∑_{d ∣ n} d^(k-1)) a₀(f).