The composite of two nebentypus-twisted slash sums #
HeckeSlash/Composition.lean computes the composite of two unweighted slash sums. This file is
the weighted counterpart. It first proves the general multiplicity-weighted formula, by
partitioning all products according to the double coset they meet, and then specialises to a
product supported on a single double coset. The statements are bundled both for functions and as
endomorphisms of the character space.
⚠ The multiplicity in the general formula is
m(D₂⁻¹, D₁⁻¹; D⁻¹), because the slash sum uses right cosets whereas the Hecke-ring structure
constants use left cosets. Consequently the formula is not by itself a ring homomorphism from the
existing Hecke ring: identifying this right-coset coefficient with the relevant structure
constant is a further step. Nor can the unrestricted twistedHeckeSlashRingLinearMap on all of
ℍ → ℂ be multiplicative, since the composition identity requires the input to lie in
functionCharSpace k χ.
Why the weights multiply, and why that is the whole point #
delta0NebentypusChar N χ is a MonoidHom on Δ₀(N), so the weight of a product of
representatives is the product of their weights. The composite of the two twisted sums is
therefore a sum over products a_v b_w weighted by the character of that product — exactly the
shape a single twisted sum over a third double coset has, which is what makes the collapse
possible. Changing representatives changes the weights attached to them, so that collapse needs
genuine representative-independence; that is Nebentypus/Independence.lean, and this file consumes
it.
Where the positivity hypothesis comes from #
Unlike the unweighted statements, the weighted ones carry 0 < det x: the weight has to pass
through the slash by x, which is ModularForm.rat_smul_slash_of_det_pos. No caller is
inconvenienced — over the chosen representatives it is det_rightCosetRep_pos_of_delta0, and over
a free family it follows from the Δ₀(N) membership those statements already require.
Why the operator lives on the character space #
twistedHeckeSlashSumEnd is an endomorphism of all of ℍ → ℂ, and on that carrier the
multiplicativity below is simply false: the underlying identity needs f to be a χ-eigenfunction.
functionCharSpace is an invariant subspace, by twistedHeckeSlashSum_mem_functionCharSpace, so
the operator restricts to it — and there the operators do multiply. This mirrors the untwisted
development, which states its operator-level results on ModularForm/CuspForm for the same
reason: that is the carrier on which the hypothesis comes for free.
Main definitions #
This file introduces no definitions; the extension it reads the composition theorem through,
twistedHeckeSlashRingCharLinearMap, is defined in Nebentypus/CharRing.lean.
Main results #
HeckeRing.GL2.twistedHeckeSlashSum_slash: slashing a twisted sum multiplies the representatives on the right, the weights riding along unchanged.HeckeRing.GL2.twistedHeckeSlashSum_twistedHeckeSlashSum: the composite of two twisted sums, as a double sum over products of representatives weighted by the character of the product.HeckeRing.GL2.twistedHeckeSlashSum_twistedHeckeSlashSum_eq_sum_nsmul: the general composite, grouped by output double coset and weighted by Shimura's multiplicity.HeckeRing.GL2.twistedHeckeSlashSumCharEnd_mul_eq_sum_nsmul: the same formula bundled on the character space.HeckeRing.GL2.twistedHeckeSlashSum_twistedHeckeSlashSum_eq_sum_of_rightCosets: the same composite over any families of representatives of the right cosets.HeckeRing.GL2.twistedHeckeSlashSum_twistedHeckeSlashSum_eq_twistedHeckeSlashSum: the collapse onto a single twisted sum, when the product set is one double coset and the products meet each of its right cosets once.HeckeRing.GL2.twistedHeckeSlashSumCharEnd_mul_of_doubleCoset_eq_mul: the pay-off — the twisted Hecke operators multiply.HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap_mul_single_single: the ring-level reading of that pay-off — a conditional anti-multiplicativity identity on basis elements. Under the same collapse and injectivity hypotheses, the image ofsingle D₁ 1 * single D₂ 1is the composite of the images in the opposite order. It is not a multiplicative action of the Hecke ring: basis elements only, under those hypotheses, and no ring homomorphism follows.
Provenance #
twistedHeckeSlashRingCharLinearMap_mul_single_single is adapted from the same project's
twistedHeckeSumFunction_mul (line 917), with two departures: the source proves multiplicativity
for arbitrary ring elements, reaching it through its own fibre-counting chain (lines 601-801,
which this repository does not carry), so what is stated here is the basis-element form the
generator-level theorem above supports, with the collapse hypotheses explicit; and the statement
shape follows main's own untwisted
heckeSlashGamma1RingModularFormLinearMap_mul_single_single (HeckeSlash/Composition.lean).
The weight-multiplication that twistedHeckeSlashSum_twistedHeckeSlashSum turns on is the content
of delta0NebentypusWeight_mul_eq_tripleDelta (line 478) in the AINTLIB LeanModularForms project
(LeanModularForms/HeckeRIngs/GL2/Unified/TwistedHeckeRing.lean, Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08). It is not
ported: with Delta0UpperUnit a MonoidHom — and hence delta0NebentypusChar one too — it is
map_mul, so it appears inline in the proof rather than as a declaration. That is the same
substitution which removed the source's delta0UpperUnit_mul and delta0IntegralMatrix_mul from
the invariance rung.
twistedHeckeSlashSum_slash has no counterpart in the source to adapt: it is the weighted
analogue of this repository's own heckeSlashSum_slash. AINTLIB reaches the same effect through
twistedHeckeSlashGen_slash_distrib (:399), which sits inside the adjugate-and-correction block
that the campaign routes around because this repository's substrate supersedes it.
twistedHeckeSlashSumCharEnd_mul_of_doubleCoset_eq_mul is the source's payoff
twistedHeckeSlashGen_comp (:801) — the source's twistedHeckeSlashGen is this repository's
twistedHeckeSlashSum. One hypothesis is deliberately not reproduced: the source assumes the
two Hecke-ring generators commute, because it states the payoff at ring level where their product
order is ambiguous. Stated at operator level the order is fixed by the statement — Module.End
multiplies by composition, so D₁ acts first — exactly as the untwisted
heckeSlashGamma1ModularFormEnd_mul_of_doubleCoset_eq_mul does, and the hypothesis has nothing
left to do.
The multiplicity-weighted theorem corresponds to AINTLIB's
twistedHeckeSlashGen_comp_eq_m_sum in the same file.
⚠ Not adapted, so that the source line numbers are not read as a wider claim:
twisted_weighted_slash_product_eq (:494) is a per-pair step that carries a summand into a third
double coset under an assumed twisted invariance of f; the route here goes through
representative-independence instead. The source's correction-map fibre block (:629, :661,
:710) is not adapted either — its bookkeeping is already available untwisted and more generally in
HeckeSlash/Composition.lean with the HeckeRing/Multiplicity module.
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4: the displayed computation preceding Proposition 3.37 is the composite below.
Slashing a twisted slash sum multiplies the representatives on the right, the weights
riding along unchanged. The weighted counterpart of heckeSlashSum_slash, which needs no
hypothesis at all; here 0 < det x is what lets each weight pass through the slash by x.
The composite of two twisted slash sums, over the representatives they are defined with,
for an arbitrary f : ℍ → ℂ.
The weight on the summand at (v, w) is the character of the product a_v b_w, because
delta0NebentypusChar is a MonoidHom and the two weights therefore multiply. That is what makes
this a candidate for collapsing onto a single twisted sum over a third double coset. That collapse
needs twisted representative-independence, so it is not available at this point in the file; it is
twistedHeckeSlashSum_twistedHeckeSlashSum_eq_twistedHeckeSlashSum in the Free section below.
The multiplicity-weighted composite of two twisted slash sums. On a χ-eigenfunction,
the composite is the sum over the double cosets met by products of representatives, with each
twisted slash sum scaled by the common number of times its right cosets occur:
T_{D₂}(T_{D₁} f) = ∑_D m(D₂⁻¹, D₁⁻¹; D⁻¹) • T_D f.
The reversed and inverted arguments are forced by the right-coset convention of the slash sum:
inversion turns its collision count into the left-coset count defining
DoubleCoset.multiplicity. This is the weighted counterpart of
heckeSlashSum_heckeSlashSum_eq_sum_nsmul; the character weight is constant on each right coset
only after it is paired with the slash, by smul_slash_eq_of_rightCoset_eq.
The multiplicity-weighted composition law on the character space. This is
twistedHeckeSlashSum_twistedHeckeSlashSum_eq_sum_nsmul bundled as an equality of endomorphisms
of functionCharSpace k χ. The order on the left records that D₁ acts first.
The multiplicativity of the twisted slash sum, over any families of representatives. For a
χ-eigenfunction f and families (aᵢ), (bⱼ) of representatives of the right cosets of the two
double cosets,
twistedHeckeSlashSum k χ D₂ (twistedHeckeSlashSum k χ D₁ f) = ∑_{i,j} χ'(aᵢ bⱼ) • (f ∣[k] aᵢ bⱼ),
writing χ' for delta0NebentypusChar N χ: the summand at (i, j) is weighted by the character of
the product.
The weighted counterpart of heckeSlashSum_heckeSlashSum_eq_sum_of_rightCosets, and the free-family
form of twistedHeckeSlashSum_twistedHeckeSlashSum above. The eigenfunction property is used twice,
exactly as invariance is there: once to evaluate the inner sum on (aᵢ), and once — through
twistedHeckeSlashSum_mem_functionCharSpace — to know the inner sum is itself a χ-eigenfunction,
which is what lets the outer sum be evaluated on (bⱼ).
The weights multiply because delta0NebentypusChar is a MonoidHom, and ℂ is commutative, so the
two factors combine into the character of the product regardless of the order they are met in.
The composite of two twisted slash sums is the twisted slash sum 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.
This is the collapse, for a χ-eigenfunction f — the identity is false without hf, as the
module docstring records. The weighted counterpart of
heckeSlashSum_heckeSlashSum_eq_heckeSlashSum, and its two hypotheses play the same roles: hD₃
says the product set is the single coset D₃, and hinj₃ says the products have no right-coset
collisions. This does not identify hinj₃ with the left-representative count used by
DoubleCoset.multiplicity. The covering half that
twistedHeckeSlashSum_eq_sum_of_rightCosets would otherwise need is automatic, by
doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets.
The products lie in Δ₀(N) because each factor does and Δ₀(N) is a submonoid, which is what lets
the twisting character be applied to them.
The twisted Hecke operators multiply. On the character space, and when the product set is
the single double coset D₃ with no right-coset collisions among the products, the composite of
the operators of D₁ and D₂ is the operator of D₃.
This is the generator-level input that a multiplicativity proof for
twistedHeckeSlashRingLinearMap would consume; it does not itself close that gap, which concerns
arbitrary Hecke-ring elements on all of ℍ → ℂ. It is the weighted counterpart of
heckeSlashGamma1ModularFormEnd_mul_of_doubleCoset_eq_mul, and it is stated on the character space
for the same reason that one is stated on ModularForm: that is the carrier on which the
hypothesis the underlying identity needs — here f ∈ functionCharSpace, there Γ₁-invariance —
comes for free.
As there, Module.End multiplies by composition, so D₁ acts first on the right-hand side of the
underlying identity; that is the order recorded here. The source states this with a hypothesis that
the two Hecke-ring generators commute; no such hypothesis is needed once the order is fixed by the
statement.
A conditional anti-multiplicativity identity on basis elements. When the product of the two
double cosets is again a single double coset with no right-coset collisions, the image of
single D₁ 1 * single D₂ 1 is the composite of the images in the opposite order. Stated for basis
elements only, under those hypotheses; this is not a multiplicative action of the Hecke ring, and
no ring homomorphism follows from it.
The ring-level reading of twistedHeckeSlashSumCharEnd_mul_of_doubleCoset_eq_mul above: the two
criteria line up, one on each side, with HeckeCosetModule.mul_single_single_of_mulMap_eq
supplying the product in the Hecke ring and the composition theorem supplying it in Module.End.
Module.End multiplies by composition and the slash acts on the right, so the basis element D₁
of the left factor is the operator applied first — the map is an anti-homomorphism on these
elements, matching heckeSlashGamma1RingModularFormLinearMap_mul_single_single for the untwisted
Γ₁(N) operators.