The nebentypus-twisted slash sum over a double coset of Γ₀(N) #
HeckeSlash/Basic.lean sums f ∣[k] aᵥ over representatives of the right cosets a double coset
decomposes into, with no weights at all, and HeckeSlash/Gamma0.lean instantiates that at
Γ₀(N). That instantiation stops short of the character on purpose: Γ₀(N) is where the
nebentypus lives, so there is a second, weighted sum to be had, and this file is it. Each summand
is multiplied by delta0NebentypusChar χ of its own representative, which Δ₀(N) contains.
Which way the character goes #
The weight is the character itself, not its inverse, and that is forced by the convention
Delta0UpperUnit was defined with rather than chosen here. Delta0UpperUnit reads off the
upper-left unit, so on Γ₀(N) it is the inverse of the lower-right unit Gamma0Map records
(Delta0UpperUnit_mapGL: ad ≡ 1 there), and delta0NebentypusChar_mapGL carries that inverse
through χ. Classically the twisted operator divides by the nebentypus; composing the two
inversions, dividing by χ ∘ Gamma0Map is multiplying by delta0NebentypusChar χ, so the
inverse appears nowhere in the sum below. Reading the weight as the nebentypus extended along
Gamma0Map and adding an inverse to compensate would negate the twist twice over.
⚠ The pay-off of the weighting is not proved here. What makes the twisted sum the useful one
is that it is well defined on, and preserves, the character space modFormCharSpace k χ — the
weights cancel the eigenvalue χ that mem_modFormCharSpace_iff_nebentypus records, which the
unweighted heckeSlashSum cannot do. Like heckeSlashSum before it, what is established below
is only the definition and its linearity in f; every statement here holds for an arbitrary
f : ℍ → ℂ, and none of them mentions a character space.
Main definitions #
HeckeRing.GL2.nebentypusWeight: the weightdelta0NebentypusChar χ aᵥa summand carries.HeckeRing.GL2.twistedHeckeSlashSum: the weighted sum∑ᵥ delta0NebentypusChar χ aᵥ • (f ∣[k] aᵥ).HeckeRing.GL2.twistedHeckeSlashSumEnd: that sum bundled as aℂ-linear endomorphism ofℍ → ℂ, the form downstream constructions consume.
Main results #
HeckeRing.GL2.twistedHeckeSlashSum_add,HeckeRing.GL2.twistedHeckeSlashSum_zero,HeckeRing.GL2.twistedHeckeSlashSum_smul: the twisted sum isℂ-linear inf. Unlike the unweighted sum, homogeneity needs no positivity hypothesis from the caller: the representatives lie inΔ₀(N), whose determinants are positive.HeckeRing.GL2.twistedHeckeSlashSum_eq_heckeSlashSum: at the trivial character the twisted sum is the unweightedheckeSlashSum.
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5 (Hecke operators with nebentypus).
- Adapted from the AINTLIB
LeanModularFormsproject (Chris Birkbeck),HeckeRIngs/GL2/Unified/TwistedHeckeRing.leanat commit2baa76f742bdb4fb8ee323fabba41203bd390e08, declarationsdeltaRepGen,delta0NebentypusWeight,twistedHeckeSlashGen,twistedHeckeSlashGen_addandtwistedHeckeSlashGen_smul. The source sums over adjugated representatives indexed by its own quotient and carries an explicit inverse on each weight; here the representatives areHeckeSlash/Basic.lean'srightCosetRep, and the inverse is absent for the reason above.
The weight a summand carries: the twisting character delta0NebentypusChar χ evaluated
on the summand's own representative. Naming it keeps rightCosetRep_mem_Delta0 out of every
statement downstream, since the character is a homomorphism on the submonoid and so needs the
membership proof as data.
Equations
Instances For
Defining equation for nebentypusWeight. Since the definition sits in a public section
without @[expose], a downstream module rewrites with this instead of unfolding the body.
The enumeration ∑ needs, obtained from the ambient Finite instance by choice. As in
HeckeSlash/Basic.lean it is local and noncomputable: nothing below depends on which
enumeration is chosen, so no declaration should carry one as data.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The nebentypus-twisted slash sum over a double coset of Γ₀(N):
∑ᵥ delta0NebentypusChar χ aᵥ • (f ∣[k] aᵥ) over the same representatives aᵥ = δ τᵥ⁻¹ that
the unweighted heckeSlashSum runs over, each summand weighted by the twisting character of its
own representative.
⚠ Like heckeSlashSum, the definition depends on the chosen representatives D.out and
v.out, and on a general f : ℍ → ℂ the value changes with them; the weights are attached to
the representatives, not to the cosets. What repairs that is the twisted invariance of f, in
the same way Γ₁-invariance repairs the unweighted sum, and it is not proved here.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Defining equation for twistedHeckeSlashSum at the level of functions. Since the definition
is not @[expose], a downstream module rewrites with this instead of unfolding the body; the
pointwise twistedHeckeSlashSum_apply below is the companion for arguments that work at a
point.
The pointwise value of the twisted slash sum: the weights scale the slashed values one by one, so the scalar sits inside the sum and outside the evaluation.
At the trivial character the twisted slash sum is the unweighted one: every weight
nebentypusWeight 1 D v is 1, so the sum is heckeSlashSum over the same representatives.
The twisted slash sum is additive in f.
The twisted slash sum kills the zero function.
The twisted slash sum is homogeneous in f. With twistedHeckeSlashSum_add this gives
ℂ-linearity.
The positivity the scalar needs to pass through the slash is det_rightCosetRep_pos_of_delta0,
which holds outright at this level, so no hypothesis is asked of the caller.
Stated for a complex scalar only, where heckeSlashSum_smul admits any α acting on ℂ
through the scalar tower. The weights here are complex, so such an α-scalar would additionally
have to commute past them — SMulCommClass ℂ α ℂ does not follow from DistribSMul α ℂ plus
IsScalarTower α ℂ ℂ — and ℂ is the field the character space is a module over, so nothing
downstream asks for more.
The twisted slash sum as a ℂ-linear endomorphism of ℍ → ℂ. Bundling it as a
Module.End ℂ is what lets a downstream construction consume the operator directly, instead of
re-bundling this map and re-proving its linearity; the two fields are exactly
twistedHeckeSlashSum_add and twistedHeckeSlashSum_smul.
⚠ This is an endomorphism of all functions ℍ → ℂ, not of the character space
modFormCharSpace k χ. That the twisted sum is well defined on, and preserves, that subspace is
the pay-off of the weighting, and — as everywhere in this file — it is not proved here.
Equations
- HeckeRing.GL2.twistedHeckeSlashSumEnd k χ D = { toFun := HeckeRing.GL2.twistedHeckeSlashSum k χ D, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The endomorphism is twistedHeckeSlashSum on underlying functions. This characterises it
directly, without exposing the bundling.