The slash sum of an invariant function depends only on the double coset #
heckeSlashSum k D f is a sum over the chosen representatives D.out of the double coset and
v.out of its right cosets, and HeckeSlash/Basic.lean records that on a general f : ℍ → ℂ
the value moves with those choices. This file proves that for a Γ₁-invariant f it does not:
the sum is ∑ᵢ f ∣[k] aᵢ for any family (aᵢ) of representatives of the right cosets of
Γ₁ δ Γ₂, whatever δ in the double coset and whatever representatives are used to name them.
That is what makes the endomorphisms of HeckeSlash/ModularForm.lean operators attached to the
double coset rather than to a presentation of it, and it is Shimura's definition (§3.4, (3.4.1)),
which fixes no representatives at all.
What the choice-freeness rests on #
Two families of representatives of the same right cosets differ, coset by coset, by a factor of
Γ₁ on the left, and f ∣[k] (γ₁ x) = (f ∣[k] γ₁) ∣[k] x = f ∣[k] x for γ₁ ∈ Γ₁ when f
is Γ₁-invariant: that is slash_eq_of_rightCoset_eq, and it is the only place invariance is
used. Everything else is a comparison of two enumerations of the same finite set of right
cosets: DoubleCoset.doubleCoset_eq_iUnion_rightCosets says the chosen representatives cover
the double coset and DoubleCoset.op_mul_out_inv_smul_injective says they do so without
repetition, which are exactly the two hypotheses demanded of the family (aᵢ), so the two
enumerations are matched by a bijection and the sums agree term by term.
The hypotheses are stated with MulOpposite.op x • (Γ₁ : Set _) — Mathlib's spelling of the
right coset Γ₁ x — so that the two lemmas above are literally what a caller supplies. The
double coset Γ₁ δ Γ₂ is named as doubleCoset (D.out : GL (Fin 2) ℚ) Γ₁ Γ₂; that set
depends on no choice, since DoubleCoset.doubleCoset_eq_of_mem gives the same set for every
δ in it, and heckeSlashSum_eq_sum_of_mem_doubleCoset is the resulting statement that any
such δ may be used to form the sum.
Repetition, and where it comes from #
heckeSlashSum_eq_sum_of_rightCosets asks its family to name each right coset exactly once. The
composite of two slash sums does not: heckeSlashSum_heckeSlashSum_eq_sum_of_rightCosets
(HeckeSlash/Composition.lean) presents that composite as a sum over pairs of representatives,
and the products aᵢ bⱼ landing in one double coset name each of its right cosets not once but a
fixed number of times — Shimura's multiplicity, by
DoubleCoset.card_pairs_mem_rightCoset_eq_multiplicity and
DoubleCoset.card_pairs_mem_rightCoset_congr. So the last statement below trades injectivity for
that uniform repetition count and concludes a multiple of the slash sum, which is the form each
double coset contributes to the multiplicity-weighted composite ∑_D m(D₁, D₂; D) · T_D.
Main results #
HeckeRing.GL2.slash_eq_of_rightCoset_eq: slashing aΓ₁-invariant function byxdepends only on the right cosetΓ₁ x.HeckeRing.GL2.heckeSlashSum_eq_sum_of_rightCosets: the choice-free description of the slash sum. ForΓ₁-invariantf,heckeSlashSum k D f = ∑ᵢ f ∣[k] aᵢfor any family(aᵢ)whose right cosetsΓ₁ aᵢare distinct and cover the double coset.HeckeRing.GL2.heckeSlashSum_eq_sum_of_mem_doubleCoset: the special case that fixes the choice of double-coset representative only: anyδ ∈ Γ₁ D.out Γ₂gives the same sum.HeckeRing.GL2.sum_slash_eq_nsmul_heckeSlashSum: the weighted collapse. A family naming each right coset of the double coset exactlymtimes — repetitions allowed, covering not assumed — sums tom • heckeSlashSum k D f.HeckeRing.GL2.sum_slash_coe_eq_nsmul_heckeSlashSum: the weighted collapse for a form, whose slash-invariance dischargeshf.HeckeRing.GL2.heckeSlashSum_coe_eq_sum_of_rightCosets: the same description for a form of levelG.map (mapGL ℝ), whose slash-invariance discharges the hypothesishf. It is whatHeckeSlash/ModularForm.leanreads off the two exported endomorphisms with, incoe_heckeSlashModularFormEnd_eq_sumandcoe_heckeSlashCuspFormEnd_eq_sum.
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions,
§3.4: (3.4.1) defines
f ∣[Γ₁ α Γ₂]ₖas the sum over a decompositionΓ₁ α Γ₂ = ⊔ᵥ Γ₁ aᵥ, and observes that it is independent of the decomposition chosen.
Slashing a Γ₁-invariant function depends only on the right coset. If Γ₁ x = Γ₁ y
then f ∣[k] x = f ∣[k] y, because y = (y x⁻¹) x with y x⁻¹ ∈ Γ₁ and the slash by that
factor is trivial on f.
This is the whole role invariance plays in the choice-freeness below: everything else is a comparison of two enumerations of the same set of cosets.
The slash sum of a Γ₁-invariant function is the sum over any decomposition of the double
coset into right cosets. If the right cosets Γ₁ aᵢ are pairwise distinct and cover
Γ₁ D.out Γ₂, then heckeSlashSum k D f = ∑ᵢ f ∣[k] aᵢ.
So the operator is attached to the double coset itself: the representatives D.out and v.out
that heckeSlashSum happens to pick are one such family (doubleCoset_eq_iUnion_rightCosets and
op_mul_out_inv_smul_injective), and every other family gives the same function.
Invariance of f under Γ₁ is what the proof uses, once, through
slash_eq_of_rightCoset_eq; on a general f the statement is false, as HeckeSlash/Basic.lean
records.
The slash sum may be formed from any representative of the double coset. For δ in
Γ₁ D.out Γ₂ and Γ₁-invariant f, summing f ∣[k] (δ τᵥ⁻¹) over Γ₂ ⧸ (Γ₂ ∩ δ⁻¹Γ₁δ) gives
heckeSlashSum k D f again — the representative heckeSlashSum picks is in no way
distinguished.
This is heckeSlashSum_eq_sum_of_rightCosets at the family Shimura's decomposition of
Γ₁ δ Γ₂ provides, the double coset of δ being that of D.out
(DoubleCoset.doubleCoset_eq_of_mem).
A family naming each right coset the same number of times sums to a multiple of the slash
sum. In place of the injectivity of heckeSlashSum_eq_sum_of_rightCosets, ask that every right
coset of the double coset be named by exactly m members of the family: then the sum over the
family is m • heckeSlashSum k D f.
Covering is not a hypothesis. A right coset named by no member forces m = 0, and then both
sides vanish; for m ≠ 0 the family does cover, so nothing is lost by leaving it out and a user
holding only a set of products need not prove it.
This is the shape the composite of two slash sums arrives in. Grouping the products aᵢ bⱼ of
heckeSlashSum_heckeSlashSum_eq_sum_of_rightCosets by the double coset they lie in, the group
belonging to one double coset meets each of that coset's right cosets the same number of times
(DoubleCoset.card_pairs_mem_rightCoset_congr), and that common count is Shimura's multiplicity
(DoubleCoset.card_pairs_mem_rightCoset_eq_multiplicity) — so each group contributes
m(D₁, D₂; D) • heckeSlashSum k D f.
The slash sum of a form of level G.map (mapGL ℝ) is the sum over any decomposition of the
double coset into right cosets. This is heckeSlashSum_eq_sum_of_rightCosets with the
hypothesis hf discharged: a form of that level is slash-invariant under G.map (mapGL ℚ) by
ModularForm.slash_eq_of_mem_map_mapGL, the ℚ/ℝ bridge.
F is any type of slash-invariant forms, so this covers SlashInvariantForm, ModularForm and
CuspForm at once; combined with the coe_heckeSlash…End lemmas it describes the endomorphisms
built from a double coset, at any level, without reference to the representatives they are
assembled from.
The weighted collapse for a form of level G.map (mapGL ℝ). This is
sum_slash_eq_nsmul_heckeSlashSum with the hypothesis hf discharged, exactly as
heckeSlashSum_coe_eq_sum_of_rightCosets discharges it for the unweighted statement: a form of
that level is slash-invariant under G.map (mapGL ℚ) by ModularForm.slash_eq_of_mem_map_mapGL.
F is any type of slash-invariant forms, so this covers SlashInvariantForm, ModularForm and
CuspForm at once, and a consumer working on a character space need not rebuild the invariance
bridge.