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 companion of HeckeSlash/Gamma1.lean
at the larger group.
Both side conditions the general construction carries are discharged once, and neither is specific
to the level: the Hecke triple is HeckeRing/GL2/Gamma0/Basic.lean's instance, which also supplies
the finiteness of the right-coset index, and the positivity hypothesis is
out_mem_glpos_of_delta0 from that same file — 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_heckeSlashGamma0ModularFormEnd and coe_heckeSlashGamma0CuspFormEnd rewrite the
modular-form and cusp-form operator respectively to heckeSlashSum, and
heckeSlashSum_coe_eq_sum_of_rightCosets (HeckeSlash/Independence.lean) then evaluates that on
any decomposition of Γ₀(N) δ Γ₀(N) into right cosets.
⚠ These are the operators of an arbitrary double coset, and they carry no character.
Γ₀(N) is where the nebentypus lives, so the twisted operators — the ones weighted by
χ ∘ Delta0UpperUnit, acting on modFormCharSpace k χ rather than on all of
M_k(Γ₀(N)) — are a different construction built on top of these. This file deliberately stops
short of that: it is the untwisted Γ₀(N) instantiation, matching Gamma1.lean declaration for
declaration.
⚠ Identifying particular cosets with the classical Tₙ is likewise a separate milestone and is
not proved here.
Main definitions #
HeckeRing.GL2.heckeSlashGamma0ModularFormEnd: the operator onM_k(Γ₀(N)).HeckeRing.GL2.heckeSlashGamma0CuspFormEnd: the operator onS_k(Γ₀(N)).
Main results #
HeckeRing.GL2.rightCosetRep_mem_Delta0: the representatives of the right cosets a double coset decomposes into lie inΔ₀(N).HeckeRing.GL2.det_rightCosetRep_pos_of_delta0: they therefore have positive determinant, with no hypothesis on the coset or on the flanking group.HeckeRing.GL2.coe_heckeSlashGamma0ModularFormEnd,HeckeRing.GL2.coe_heckeSlashGamma0CuspFormEnd: both operators areheckeSlashSumon underlying functions.
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.
The representatives lie in Δ₀(N). rightCosetRep D v is δ τᵥ⁻¹ with δ ∈ Δ₀(N) and
τᵥ in the flanking copy of Γ₀(N), which is a subgroup of Δ₀(N) — Gamma0Image_le_Delta0 —
so the inverse stays inside it.
Both flanks being Γ₀(N) is what makes this hypothesis-free. The same statement holds for any
flanking Γ₂ ≤ Δ₀(N), but only at the cost of an explicit containment hypothesis every caller
would have to discharge, and no such caller exists; contrast out_mem_glpos_of_delta0, which is
generic in both flanks because there it costs nothing.
The representatives have positive determinant. They lie in Δ₀(N), and every element of
Δ₀(N) is an integral matrix of positive determinant, so — unlike for the unweighted
heckeSlashSum_smul — no caller has to supply this.
The Hecke operator of a double coset on M_k(Γ₀(N)): 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
Instances For
The Hecke operator of a double coset on S_k(Γ₀(N)) — the statement that the operator
above preserves cuspidality.
Equations
Instances For
The operator is heckeSlashSum on underlying functions.
The operator is heckeSlashSum on underlying functions.