Composing the slash sums of two double cosets #
HeckeSlash/Basic.lean attaches to a double coset Γ₁ δ Γ₂ = ⊔ᵥ Γ₁ aᵥ the slash sum
f ∣[Γ₁ δ Γ₂]ₖ = ∑ᵥ f ∣[k] aᵥ, and HeckeSlash/Invariance.lean shows the result is
Γ₂-invariant, so a second double coset Γ₂ δ₂ Γ₃ may be applied to it. This file computes that
composite: it is the double sum over the products of the two families of representatives,
(f ∣[Γ₁ δ₁ Γ₂]ₖ) ∣[Γ₂ δ₂ Γ₃]ₖ = ∑_{i, j} f ∣[k] (aᵢ bⱼ),
which is the multiplicative half of Shimura's §3.4 and the engine behind his Proposition 3.37.
HeckeSlash/Ring.lean and HeckeSlash/CuspRing.lean both record that its absence is what
confines the action of the abstract Hecke ring on M_k(Γ₁(N)) and S_k(Γ₁(N)) to a ℤ-linear
map rather than a ring homomorphism.
The two statements, and what each costs #
The identity above is proved twice, because two different things are being asserted.
With the chosen representatives (heckeSlashSum_heckeSlashSum) it is pure bookkeeping and
needs no hypothesis on f at all: slashing distributes over a finite sum
(SlashAction.sum_slash) and f ∣[k] (a b) = (f ∣[k] a) ∣[k] b is SlashAction.slash_mul.
With arbitrary representatives (heckeSlashSum_heckeSlashSum_eq_sum_of_rightCosets) it needs
f to be Γ₁-invariant, twice over: once so that the inner sum may be read off the family
(aᵢ) (heckeSlashSum_eq_sum_of_rightCosets), and once more because the outer sum is read
off (bⱼ), which requires the inner sum to be Γ₂-invariant — that is
heckeSlashSum_slash_invariant, and it is the only place the two flanking groups have to be
matched.
Which right cosets the products aᵢ bⱼ run over is a set-level question with no slash action in
it, so it is answered where the rest of the double-coset vocabulary lives: they cover the
product set Γ₁ δ₁ Γ₂ · Γ₂ δ₂ Γ₃, by
DoubleCoset.doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets (HeckeRing/Basic.lean). They do
so with repetition, which is why the criterion below has to be told separately that the cosets
are distinct. How often each right coset is met is counted by
DoubleCoset.card_pairs_mem_rightCoset_eq_multiplicity, which identifies that count with
DoubleCoset.multiplicity. Since the multiplicity counts left-coset representatives, the
identification inverts all three arguments and exchanges the two factors; the group-theoretic
content of it is a statement about the group alone, proved with the multiplicity API itself.
What this does and does not give #
Putting these together gives the criterion heckeSlashSum_heckeSlashSum_eq_heckeSlashSum:
if the product set is a single double coset Γ₁ δ₃ Γ₃ and the pairs (i, j) do meet each of
its right cosets exactly once, then the composite operator is the operator of Γ₁ δ₃ Γ₃. At
Γ₁ = Γ₂ = Γ₃ = Γ₁(N) this is heckeSlashGamma1ModularFormEnd_mul_of_doubleCoset_eq_mul and
its cusp-form companion. The criterion is formally analogous to the ring-side
single-basis-element criterion HeckeCosetModule.mul_single_single_of_mulMap_eq, and the two
are identified here: heckeSlashGamma1RingModularFormLinearMap_mul_single_single and its
cusp-form companion apply both criteria at once, so the ring product of two basis elements maps
to the composite of their operators.
The general multiplicity-weighted statement — the composite as ∑_D m(D₁, D₂; D) · T_D — is
heckeSlashSum_heckeSlashSum_eq_sum_nsmul. It partitions the pairs (v, w) by the double coset
their product lies in, which is what HeckeRing.GL2.pairCoset (HeckeRing/GL2/PairCoset.lean)
names; the double cosets met are the image of the finite type of pairs under that map, so no
finiteness beyond that of the two index types is needed. Its counting ingredient is
HeckeRing.GL2.card_pairs_pairCoset_rightCoset_eq_multiplicity from the same file: each right
coset of a fixed D is met by the same number of pairs, and that number is the multiplicity. The
bookkeeping is shared with the Hecke operators on modular symbols, which is why it is not here.
⚠ The ring homomorphism 𝕋 → Module.End is still not built here, and the remaining gap is
wider than a change of notation. HeckeCosetModule.structureConstants weights D by
DoubleCoset.multiplicity Γ₁ Γ₂ Γ₃ δ₁ δ₂ δ₃, whereas the sum below weights it by
DoubleCoset.multiplicity Γ₃ Γ₂ Γ₁ δ₂⁻¹ δ₁⁻¹ δ₃⁻¹ — the factors exchanged and all three
arguments inverted, which is what the right-coset indexing of a slash sum forces. These are
not equal, and no symmetry of multiplicity identifies them: the two counts run over
Γ ⧸ (Γ ∩ gΓ'g⁻¹) and Γ ⧸ (Γ ∩ g⁻¹Γ'g), the two degrees of a double coset, and those
differ in general. Closing the gap needs an anti-involution rather than a rewriting of
coefficients; HeckeRing/GLn/TransposeAntiInvolution.lean supplies one at level SLₙ(ℤ), and
it is what makes the Hecke ring commutative there (Shimura's Proposition 3.8).
Main results #
HeckeRing.GL2.heckeSlashSum_slash: slashing a slash sum byxmultiplies each representative byxon the right.HeckeRing.GL2.heckeSlashSum_heckeSlashSum: the composite of two slash sums, over the chosen representatives, with no hypothesis onf.HeckeRing.GL2.heckeSlashSum_heckeSlashSum_eq_sum_of_rightCosets: the multiplicativity of the slash sum, over arbitrary representatives, for aΓ₁-invariantf.HeckeRing.GL2.heckeSlashSum_heckeSlashSum_eq_heckeSlashSum: the composite is the slash sum of a third double coset, when the product set is that coset and the pairs are in bijection with its right cosets.HeckeRing.GL2.heckeSlashGamma1RingModularFormLinearMap_mul_single_singleandHeckeRing.GL2.heckeSlashGamma1CuspRingLinearMap_mul_single_single: the ring-level reading of those two — the Hecke ring acts multiplicatively on basis elements whose product is a single double coset. The map is an anti-homomorphism there, sinceModule.Endcomposes.HeckeRing.GL2.heckeSlashSum_heckeSlashSum_eq_sum_nsmul: the multiplicity-weighted composite,(f ∣[Γ₁ δ₁ Γ₂]ₖ) ∣[Γ₂ δ₂ Γ₃]ₖ = ∑_D m(D₁, D₂; D) • (f ∣[Γ₁ δ₃ Γ₃]ₖ), for aΓ₁-invariantf.HeckeRing.GL2.heckeSlashGamma1ModularFormEnd_mul_of_doubleCoset_eq_mulandHeckeRing.GL2.heckeSlashGamma1CuspFormEnd_mul_of_doubleCoset_eq_mul: the same criterion for the Hecke operators of levelΓ₁(N), as an equation between endomorphisms.
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions,
§3.4: (3.4.1) defines
f ∣[Γ₁ α Γ₂]ₖ, and the displayed computation preceding Proposition 3.37 is the composite below.
Provenance #
heckeSlashSum_heckeSlashSum_eq_sum_nsmul and its fibre argument follow the corresponding
result in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0),
https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08,
LeanModularForms/HeckeRIngs/GL2/HeckeActionGeneral.lean: heckeSlash_gen_comp_sum_eq and
heckeSlash_gen_fiber_sum. That version is stated for a single HeckePair P (so
Γ₁ = Γ₂ = Γ₃), indexed by left cosets through the adjugate anti-involution its
HeckePairAction supplies, and weighted by Finsupp.sum over Hecke-ring structure constants.
The version here is at a general Hecke triple, right-coset indexed as heckeSlashSum is, needs
no anti-involution or determinant hypothesis, and takes its coefficient from
DoubleCoset.multiplicity.
Slashing a slash sum multiplies the representatives on the right. No hypothesis on f is
needed: the slash action is additive in the function and f ∣[k] (a x) = (f ∣[k] a) ∣[k] x.
The composite of two slash sums, over the representatives they are defined with. The
statement holds for an arbitrary f : ℍ → ℂ; it is the choice-dependent form of the identity,
and heckeSlashSum_heckeSlashSum_eq_sum_of_rightCosets is the statement that matters.
The multiplicativity of the slash sum. For a Γ₁-invariant f, and any families
(aᵢ), (bⱼ) of representatives of the right cosets of Γ₁ δ₁ Γ₂ and of Γ₂ δ₂ Γ₃,
(f ∣[Γ₁ δ₁ Γ₂]ₖ) ∣[Γ₂ δ₂ Γ₃]ₖ = ∑_{i, j} f ∣[k] (aᵢ bⱼ).
This is the identity Shimura computes in §3.4 on the way to Proposition 3.37, and the engine the ring homomorphism from the abstract Hecke ring is missing.
Invariance is used twice: once to evaluate the inner slash sum on the family (aᵢ), and once —
through heckeSlashSum_slash_invariant — to know that the inner sum is Γ₂-invariant, which is
what lets the outer one be evaluated on (bⱼ).
The composite is the operator of a single double coset, when the product set
Γ₁ δ₁ Γ₂ · Γ₂ δ₂ Γ₃ is that coset and the products aᵢ bⱼ meet each of its right cosets
exactly once.
The two hypotheses are formally analogous to those of
HeckeCosetModule.mul_single_single_of_mulMap_eq: hD₃ says that the product set is the single
coset D₃, while hinj₃ says that the products have no right-coset collisions. hinj₃ is
left as the bare injectivity it is used as; the collision count it rules out is identified with
DoubleCoset.multiplicity by DoubleCoset.card_pairs_mem_rightCoset_eq_multiplicity. The
covering half of the hypothesis heckeSlashSum_eq_sum_of_rightCosets would otherwise need is
automatic, by doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets.
The multiplicity-weighted composite, and with it the general form of the composition law.
For a Γ₁-invariant f, the composite of the two slash sums is the sum, over the double cosets
met by the products aᵥ b_w, of Shimura's multiplicity times the slash sum of that coset:
(f ∣[Γ₁ δ₁ Γ₂]ₖ) ∣[Γ₂ δ₂ Γ₃]ₖ = ∑_D m(D₁, D₂; D) • (f ∣[Γ₁ δ₃ Γ₃]ₖ).
heckeSlashSum_heckeSlashSum_eq_heckeSlashSum is the special case where the products meet a
single double coset and meet each of its right cosets exactly once.
This is a composition formula for the slash action, not yet the Hecke-ring homomorphism. Its
coefficient is DoubleCoset.multiplicity Γ₃ Γ₂ Γ₁ δ₂⁻¹ δ₁⁻¹ δ₃⁻¹, with the factors exchanged
and all three arguments inverted relative to HeckeCosetModule.structureConstants; as the
module docstring records, the two are not equal, and comparing them needs an anti-involution.
No finiteness is assumed beyond the two input Hecke triples. The double cosets met are the
image of a finite type under pairCoset, and the finiteness of each output coset's own
decomposition quotient — which heckeSlashSum k D f sums over — comes from the composite
triple IsHeckeTriple Δ Γ₁ Γ₃, which IsHeckeTriple.trans derives from the two given ones.
The Hecke operators of level Γ₁(N) multiply, when the product set is the single double
coset D₃ and the products of the chosen right-coset representatives have no collisions.
Module.End multiplies by composition, so D₁ acts first on the right-hand side of the
underlying identity (f ∣ D₁) ∣ D₂ = f ∣ D₃; that is the order recorded here.
The Hecke operators of level Γ₁(N) multiply on cusp forms, when the product set is the
single double coset D₃ and the products of the chosen right-coset representatives have no
collisions.
The Hecke ring acts multiplicatively on modular forms, where the product of two double
cosets is again a single double coset. The modular-form half of the pair; see
heckeSlashGamma1CuspRingLinearMap_mul_single_single for cusp forms.
The two are parallel rather than one specialising the other: the operators live in
Module.End ℂ (ModularForm ..) and Module.End ℂ (CuspForm ..) respectively, so neither
equation transports to the other, and each is proved from its own composition theorem.
The Hecke ring acts multiplicatively on cusp forms, where the product of two double cosets
is again a single double coset. This is the ring-level reading of
heckeSlashGamma1CuspFormEnd_mul_of_doubleCoset_eq_mul: the two criteria line up, one on each
side, with mul_single_single_of_mulMap_eq supplying the product in the Hecke ring and the
composition theorem supplying it in Module.End.
Note the order. Module.End multiplies by composition and the slash acts on the right, so the
basis element D₁ of the left factor becomes the operator applied first: the map is an
anti-homomorphism on these elements, not a homomorphism.
Full multiplicativity (Shimura, Proposition 3.37) is not available — it needs the structure
constants of a product that spreads over several double cosets with multiplicity, whereas both
criteria used here assume the product collapses to the single coset D₃. This lemma is the part
that is provable from what is on hand.