The twisted slash sum depends only on the double coset #
HeckeSlash/Independence.lean proves that heckeSlashSum k D f is ∑ᵢ f ∣[k] aᵢ for any
family (aᵢ) of representatives of the right cosets of Γ₁ δ Γ₂, provided f is Γ₁-invariant.
This file is the nebentypus-twisted counterpart.
Why this is a theorem and not bookkeeping #
In the untwisted setting a change of representatives moves each summand f ∣[k] aᵢ by an element
of Γ₁, and invariance absorbs it. Here f is only a χ-eigenfunction, so the slash genuinely
changes — and what repairs it is the weight: the summand carries delta0NebentypusChar χ of its
own representative, and that character factor is exactly the inverse of the eigenvalue the slash
picks up. So the weighted summand, unlike the bare slash, is a function of the right coset alone.
That cancellation is delta0NebentypusChar_smul_slash_mapGL_mul of
HeckeSlash/Nebentypus/Invariance.lean, which states it for a representative presented as
γ · x. The only work here is to feed it a right-coset equality instead, and then to run the
untwisted file's comparison of two enumerations unchanged.
Main results #
HeckeRing.GL2.smul_slash_eq_of_rightCoset_eq: the weighted slash of aχ-eigenfunction depends only on the right cosetΓ₀(N) x.HeckeRing.GL2.twistedHeckeSlashSum_eq_sum_of_rightCosets:twistedHeckeSlashSum k χ D fis the weighted sum over any family of representatives of the right cosets.HeckeRing.GL2.sum_nebentypus_smul_slash_eq_nsmul_twistedHeckeSlashSum: if a family names every right coset exactlymtimes, its weighted sum ismtimes the twisted slash sum.
Provenance #
The uniformly repeating-family theorem corresponds to the role of
twisted_filtered_sum_collapse_of_qOf in AINTLIB's
LeanModularForms/HeckeRIngs/GL2/Unified/TwistedHeckeRing.lean (Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB at commit
2baa76f742bdb4fb8ee323fabba41203bd390e08).
References #
The weighted slash depends only on the right coset. For a χ-eigenfunction f and
representatives x, y of Δ₀(N) lying in the same right coset of Γ₀(N), the weighted slashes
agree.
This is the twisted counterpart of slash_eq_of_rightCoset_eq, and it is where the whole content
of the independence below sits: there invariance makes the bare slash coset-dependent, here it is
the character weight that does it. The cancellation itself is
delta0NebentypusChar_smul_slash_mapGL_mul; all this adds is the passage from a right-coset
equality to the factorisation y = γ · x that lemma consumes.
A covering family already lies in Δ₀(N). Each aᵢ lies in its own right coset, hence in
the double coset of D.out, which the Hecke triple places back inside Δ₀(N).
So membership is not an extra hypothesis on the statements below: it is implied by the covering,
and is stated through this lemma only so that the twisting character can be applied to aᵢ without
rebuilding the proof term inside every statement.
The twisted slash sum of a χ-eigenfunction is the weighted sum over any decomposition of
the double coset into right cosets. If the right cosets Γ₀(N) aᵢ are pairwise distinct and
cover Γ₀(N) D.out Γ₀(N), and every aᵢ lies in Δ₀(N), then twistedHeckeSlashSum k χ D f is
∑ᵢ χ'(aᵢ) • (f ∣[k] aᵢ).
So the twisted operator, like the untwisted one, is attached to the double coset rather than to
the representatives twistedHeckeSlashSum happens to choose.
Unlike an earlier form of this statement, membership of the aᵢ in Δ₀(N) is not a
hypothesis: hcover already forces it, by mem_Delta0_of_cover above. The character is applied to
aᵢ through that derived term, so a caller supplies only the cover and the injectivity, exactly as
in the untwisted heckeSlashSum_eq_sum_of_rightCosets.
A uniformly repeating family gives a multiple of the twisted slash sum. Let (aᵢ) be a
family of elements in the double coset of D. If every right coset Γ₀(N) x inside D is named
by exactly m members of the family, then
∑ᵢ χ'(aᵢ) • (f ∣[k] aᵢ) = m • twistedHeckeSlashSum k χ D f
for every χ-eigenfunction f, where χ' is delta0NebentypusChar N χ.
This is the twisted counterpart of sum_slash_eq_nsmul_heckeSlashSum. Covering is not a
hypothesis: if some right coset is missed, the common multiplicity is zero, and the conclusion
still holds. The membership hypothesis puts each aᵢ in Δ₀(N) automatically, since the whole
double coset lies there.