The twisted slash sum preserves the character space #
HeckeSlash/Nebentypus/Basic.lean defines twistedHeckeSlashSum, weighting each summand of a
double-coset sum by delta0NebentypusChar χ of its own representative, and says twice over that
the point of the weighting is left unproved: the sum is meant to be well defined on, and to
preserve, the χ-invariant functions. HeckeSlash/Nebentypus/Ring.lean names that subspace,
functionCharSpace, and repeats the omission. This file supplies what both defer.
Why the weights are exactly right #
The whole proof rests on one observation. Write χ' = delta0NebentypusChar N χ, a monoid hom on
Δ₀(N), and read the summands of the twisted sum as the weighted slash χ' x • (f ∣[k] x) at
x ∈ Δ₀(N). For f in the character space and γ ∈ Γ₀(N) this quantity is unchanged when x
is multiplied on the left by γ: slashing by γ scales f by the nebentypus χ (d_γ), while the
weight picks up χ' γ, and Delta0UpperUnit_mapGL says the two are mutually inverse. So the
weighted slash is a function of the right coset Γ₀(N) x alone — which is precisely the
representative-independence the unweighted heckeSlashSum lacks on a χ-eigenfunction, and the
reason the character has to enter as χ' rather than as χ ∘ Gamma0Map.
Granted that, the argument is Shimura's Proposition 3.37 unchanged, exactly as in
HeckeSlash/Invariance.lean: right multiplication by γ permutes the right cosets, the
permutation is MulAction.toPerm at γ⁻¹, and the only new bookkeeping is that a right factor
of γ scales the weight by χ (d_γ), which comes back out of the sum as the eigenvalue the
conclusion asserts.
Main results #
HeckeRing.GL2.delta0NebentypusChar_smul_slash_mapGL_mul: the weighted slash absorbs a left factor fromΓ₀(N).HeckeRing.GL2.mul_inv_mem_Delta0: the unnormalised representativesδ h⁻¹lie inΔ₀(N).HeckeRing.GL2.delta0NebentypusChar_smul_slash_eq_nebentypusWeight_smul_slash: an unnormalised representative carries the same weighted slash as the chosen one.HeckeRing.GL2.twistedHeckeSlashSum_mem_functionCharSpace: the twisted slash sum of aχ-invariant function isχ-invariant.HeckeRing.GL2.twistedHeckeSlashSumCharEnd,HeckeRing.GL2.coe_twistedHeckeSlashSumCharEnd: the operator restricted to that invariant subspace, which is the carrier the composition results ofNebentypus/Composition.leanstate their multiplicativity on.
Provenance #
Adapted from the AINTLIB LeanModularForms project
(LeanModularForms/HeckeRIngs/GL2/Unified/TwistedHeckeRing.lean, Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08), whose
twistedHeckeSlashGen_preserves_invariant (line 457) is the theorem below, with
twisted_weighted_slash_tRep_gen_of_mem (line 319) and delta0Nebentypus_left_weight (line 391)
its per-summand and weight-transformation steps — which are, respectively, the private
nebentypusWeight_smul_slash_slash_eq_char_smul and
nebentypusWeight_eq_char_mul_delta0NebentypusChar here.
Only the statements are taken. The source reaches them through some 210 lines of
adjugate-and-correction plumbing — gamma0Correction, gamma0_adjugate_decomp_eq,
gamma0TripleDelta, slash_GL_adjugate_triple_eq_correction_slash,
gamma0TripleDelta_left_eq_h_mul_deltaRep, twistedHeckeSlashGen_perm_summand and their helpers
— which stands in for a substrate this repository already has in stronger form: the permutation
argument of HeckeSlash/Invariance.lean at an arbitrary Hecke triple, the per-summand step
slash_rightCosetRep_of_mem of HeckeSlash/Reindex.lean, and above all Delta0UpperUnit as a
MonoidHom, which makes the multiplicativity the source proves by hand (delta0UpperUnit_mul,
delta0IntegralMatrix_mul) free here. None of that plumbing is transcribed, and the source's
own delta0Nebentypus_left_weight is re-derived from that MonoidHom structure rather than
ported.
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5 (Hecke operators with nebentypus), and §3.4, Proposition 3.37 for the permutation argument.
The weighted slash absorbs a left factor from Γ₀(N). For f in the character space,
γ ∈ Γ₀(N) and x ∈ Δ₀(N), χ' (γ x) • (f ∣[k] γ x) = χ' x • (f ∣[k] x), where
χ' = delta0NebentypusChar N χ.
This is the reason the twisting works: the weighted slash depends only on the right coset
Γ₀(N) x, so the summands of twistedHeckeSlashSum do not see the representative the definition
chooses, even though f is merely a χ-eigenfunction and not invariant. The two factors that
cancel are the eigenvalue χ (d_γ) the slash picks up and the weight χ' γ, which
Delta0UpperUnit_mapGL makes its inverse.
The product is taken as a separate variable y with hxy naming it, rather than written into the
statement, so that a caller which has the factorisation in hand does not have to rewrite inside the
Δ₀(N)-membership proof the character carries as data.
The unnormalised representatives δ h⁻¹, for h anywhere in Γ₀(N), lie in Δ₀(N). This is
rightCosetRep_mem_Delta0 with the chosen representative τᵥ replaced by an arbitrary h, which
is the generality the reindexing step below needs; that lemma is the case h = τᵥ.
An unnormalised representative carries the same weighted slash as the chosen one. If h in
Γ₀(N) has class w, then the weighted slash at δ h⁻¹ is the w-th summand of
twistedHeckeSlashSum.
This is the twisted counterpart of slash_rightCosetRep_of_mem_right in HeckeSlash/Reindex.lean:
there the unweighted slash is unchanged because f is Γ₀(N)-invariant, here the weight supplies
exactly the character factor that invariance would otherwise have given. The two representatives
differ on the left by δ (h⁻¹ τ_w) δ⁻¹, which conj_mem_of_mk_eq puts in Γ₀(N), so
delta0NebentypusChar_smul_slash_mapGL_mul applies.
The class is taken as a variable w named by hcls, rather than written as ⟦h⟧, because that is
how the reindexing consumes it: there w arrives as g⁻¹ • v and hcls is
MulAction.Quotient.mk_smul_out.
The enumeration ∑ needs, chosen exactly as in HeckeSlash/Nebentypus/Basic.lean so that the
two sums are the same term.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The twisted slash sum of a χ-invariant function is χ-invariant. This is the pay-off of
the weighting, which HeckeSlash/Nebentypus/Basic.lean and HeckeSlash/Nebentypus/Ring.lean both
state and defer: twistedHeckeSlashSum k χ D maps functionCharSpace k χ into itself, so the
twisted operators live on the character space where the unweighted heckeSlashSum does not.
This is Shimura's Proposition 3.37 with the character carried through. Right multiplication by γ
permutes the right cosets, exactly as in HeckeSlash/Invariance.lean; what the weighting adds is
that a right factor of γ multiplies a summand's weight by χ (d_γ)⁻¹. That eigenvalue is common
to every summand, so it comes back out of the sum, and it is what the conclusion asserts.
The twisted slash sum as an endomorphism of the character space. twistedHeckeSlashSumEnd
is an endomorphism of all of ℍ → ℂ, and its own docstring records that this is the wrong
carrier: the point of the weighting is that the twisted sum preserves the χ-eigenspace. It does,
by twistedHeckeSlashSum_mem_functionCharSpace, so it restricts — and on this carrier, unlike on
ℍ → ℂ, the operators multiply.
Equations
Instances For
The restricted endomorphism is the twisted slash sum on underlying functions.