The slash sum descends to modular forms and to cusp forms #
Form.lean bundles the double coset as an endomorphism of
SlashInvariantForm (G.map (mapGL ℝ)) k, and flags that this is not the roadmap's Layer 2(b)
target because holomorphy and the cusp conditions are not yet carried along. This file supplies
exactly that: the two remaining structure fields.
Invariance comes from heckeSlashEnd, holomorphy from mdifferentiable_heckeSlashSum, and
boundedness at the cusps from isBoundedAt_heckeSlashSum. Because heckeSlashEnd is not
@[expose], a structure field's .toFun does not reduce to the coercion by itself, so each
such field names the coercion form with change, then rewrites by coe_heckeSlashEnd.
The cusp-form case is then derived from the modular-form one, adding only zero_at_cusps',
so neither invariance nor holomorphy is proved twice.
Both maps are also bundled as Module.End ℂ, which is the form Hecke operators are consumed in:
bundling is what lets them compose and later carry a ring structure.
The level, and what it has to satisfy #
G is any subgroup of SL(2, ℤ) whose image G.map (mapGL ℝ) is arithmetic — the hypothesis
the two cusp lemmas need, and one (Gamma1 N).map (mapGL ℝ) carries through
CongruenceSubgroup.instFiniteIndexGamma1 once N ≠ 0. This is the roadmap's Layer 2(b)
statement: at G = Γ₁(N) and Δ = Δ₀(N) the endomorphisms below are the Hecke operators of a
double coset acting on M_k(Γ₁(N)) and on S_k(Γ₁(N)), for an arbitrary double coset of the
Hecke triple, with no divisibility condition relating the level and the determinant. The
q-expansion recurrences that identify particular cosets with the classical Tₙ are separate
statements and are not proved here.
Main definitions #
HeckeRing.GL2.heckeSlashModularFormEnd: the operator onModularForm (G.map (mapGL ℝ)) k.HeckeRing.GL2.heckeSlashCuspFormEnd: the operator onCuspForm (G.map (mapGL ℝ)) k— the statement that the action preserves cuspidality.
Main results #
HeckeRing.GL2.coe_heckeSlashModularFormEnd,HeckeRing.GL2.coe_heckeSlashCuspFormEnd: both areheckeSlashSumon underlying functions.HeckeRing.GL2.coe_heckeSlashModularFormEnd_eq_sum,HeckeRing.GL2.coe_heckeSlashCuspFormEnd_eq_sum: both are the sum of the slashes over any decomposition of the double coset into right cosets, so neither depends on the representatives it is assembled from. This isheckeSlashSum_coe_eq_sum_of_rightCosets(HeckeSlash/Independence.lean) read off the two endomorphisms.
Provenance #
The shape corresponds to heckeSlashModularForm, heckeSlashCuspForm and their bundlings in the
AINTLIB LeanModularForms project
(LeanModularForms/HeckeRIngs/GL2/HeckeAction.lean,
commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck). No code is
transcribed, and the level is a general G rather than SL₂(ℤ). AINTLIB's
CuspForm.toModularForm' is not ported: mathlib already supplies the coercion, as the CoeTC
instance of ModularFormClass (Mathlib/NumberTheory/ModularForms/Basic.lean).
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions,
§3.4, Proposition 3.37:
[Γ₁ α Γ₂]ₖsendsA_k(Γ₁), G_k(Γ₁), S_k(Γ₁)intoA_k(Γ₂), G_k(Γ₂), S_k(Γ₂), instantiated here atΓ₁ = Γ₂ = G.
The double coset as a ℂ-linear endomorphism of ModularForm (G.map (mapGL ℝ)) k. This
is the form Hecke operators are consumed in: bundling is what lets them compose and later carry a
ring structure. At G = Γ₁(N) this is the roadmap's Layer 2(b) operator.
Equations
- HeckeRing.GL2.heckeSlashModularFormEnd k D hD = { toFun := HeckeRing.GL2.heckeSlashModularForm✝ k D hD, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The double coset as a ℂ-linear endomorphism of CuspForm (G.map (mapGL ℝ)) k — the
action preserves cuspidality.
Equations
- HeckeRing.GL2.heckeSlashCuspFormEnd k D hD = { toFun := HeckeRing.GL2.heckeSlashCuspForm✝ k D hD, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The endomorphism is heckeSlashSum on underlying functions.
The endomorphism is heckeSlashSum on underlying functions.
The operator on modular forms is the sum over any decomposition of the double coset into
right cosets: if the right cosets G aᵢ are pairwise distinct and cover the double coset, then
heckeSlashModularFormEnd k D hD f = ∑ᵢ f ∣[k] aᵢ. So it is attached to the double coset, not to
the representatives heckeSlashSum is assembled from; the choice-independence itself is
heckeSlashSum_coe_eq_sum_of_rightCosets (HeckeSlash/Independence.lean).
The operator on cusp forms is the sum over any decomposition of the double coset into right cosets, exactly as for modular forms.