The Hecke operators of level `Γ₁(N)` #

HeckeSlash/ModularForm.lean builds, for a subgroup G ≤ SL(2, ℤ) and a double coset of a Hecke triple whose two flanks are G.map (mapGL ℚ), the ℂ-linear endomorphisms of ModularForm (G.map (mapGL ℝ)) k and CuspForm (G.map (mapGL ℝ)) k that the coset induces. This file instantiates that at G = Γ₁(N) and Δ = Δ₀(N) — the roadmap's Layer 2(b) setting — and discharges, once, the two side conditions the general construction carries.

The Hecke triple itself is HeckeRing/GL2/Gamma1.lean's instance, and the finiteness of the right-coset index follows from it. What is left is the positivity hypothesis, and that is out_mem_glpos_of_delta0 from HeckeRing/GL2/Gamma0/Basic.lean, where it is stated for an arbitrary pair of flanks rather than for Γ₁(N): every element of Δ₀(N) has positive determinant by definition, so no double coset of this triple ever fails it.

The operators belong to the double coset itself, not to the representatives heckeSlashSum sums over: coe_heckeSlashGamma1ModularFormEnd below rewrites either of them to heckeSlashSum, and heckeSlashSum_coe_eq_sum_of_rightCosets (HeckeSlash/Independence.lean) then evaluates that on any decomposition of Γ₁(N) δ Γ₁(N) into right cosets — any representative δ of the coset, and any representatives of the cosets Γ₁(N) aᵢ — always with the same answer.

⚠ These are the operators of an arbitrary double coset. Identifying particular cosets with the classical Tₙ — the normalisation lemma for Γ₁(N) · diag(1, p) · Γ₁(N), and the q-expansion recurrences — is a separate milestone and is not proved here.

Main definitions #

HeckeRing.GL2.heckeSlashGamma1ModularFormEnd: the operator on M_k(Γ₁(N)).
HeckeRing.GL2.heckeSlashGamma1CuspFormEnd: the operator on S_k(Γ₁(N)).

Main results #

HeckeRing.GL2.coe_heckeSlashGamma1ModularFormEnd, HeckeRing.GL2.coe_heckeSlashGamma1CuspFormEnd: both operators are heckeSlashSum on underlying functions.
HeckeRing.GL2.heckeSlashGamma1ModularFormEnd_coe_cuspForm: the two operators agree under the coercion from cusp forms to modular forms.

References #

G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4, Proposition 3.37, instantiated at Γ₁ = Γ₂ = Γ₁(N).
F. Diamond and J. Shurman, A first course in modular forms, §5.2.

source

noncomputable def HeckeRing.GL2.heckeSlashGamma1ModularFormEnd {N : ℕ} [NeZero N] (k : ℤ) (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N))) :

Module.End ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The Hecke operator of a double coset on M_k(Γ₁(N)). This is the roadmap's Layer 2(b) target for ModularForm: a ℂ-linear endomorphism of the space of modular forms of level Γ₁(N) attached to an arbitrary double coset of the Hecke triple (Γ₁(N), Δ₀(N)), with no condition relating N to the determinant of the coset.

Equations