Composing the Hecke operators on modular symbols #
ModularSymbols/Hecke/Basic.lean attaches to a double coset Γ₁' δ Γ₂' = ⊔ᵥ Γ₁' aᵥ (with
Γᵢ' = Γᵢ.map (mapGL ℚ) the images of subgroups of SL(2, ℤ)) the Hecke operator
T_D : 𝕄_w(Γ₂; R) → 𝕄_w(Γ₁; R), [x] ↦ ∑ᵥ [aᵥ · x], on the modules of modular symbols. This file
computes the composite of two such operators: it is the sum over the products of the two families
of representatives,
T_{D₁} (T_{D₂} [x]) = ∑_{i, j} [(aᵢ bⱼ) · x],
the multiplicative half of Shimura's §3.4 transposed from functions on ℍ to the coinvariants.
It is the symbol-side counterpart of HeckeSlash/Composition.lean, and the two files share the
set-level bookkeeping of the products aᵢ bⱼ, none of which mentions either action: which right
cosets they cover (DoubleCoset.doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets), how often
each is met (HeckeRing.GL2.pairCoset and
HeckeRing.GL2.card_pairs_pairCoset_rightCoset_eq_multiplicity, HeckeRing/GL2/PairCoset.lean),
and how a family naming each right coset m times is counted
(DoubleCoset.card_filter_eq_of_rightCosetRep_smul_eq).
Three forms of the composition law are recorded, in increasing generality of the conclusion.
Over arbitrary representatives (heckeSymbol_heckeSymbol_mk_eq_sum_of_rightCosets), the
composite is the double sum above for any two families naming the right cosets once each; here
the action is a left action, so the products appear as aᵢ bⱼ with the representative of the
operator applied second on the left, and — unlike the slash sums — no invariance hypothesis is
needed, because the coinvariants have absorbed it. As a single operator
(heckeSymbol_comp_heckeSymbol_eq_heckeSymbol): when the product set Γ₁' δ₁ Γ₂' · Γ₂' δ₂ Γ₃'
is one double coset and the products meet each of its right cosets exactly once, the composite
is the operator of that coset. Multiplicity-weighted
(heckeSymbol_comp_heckeSymbol_eq_sum_nsmul): in general the composite is
∑_D m(D₁, D₂; D) • T_D over the double cosets the products land in, the coefficient being
Shimura's multiplicity in the right-coset-indexed form
DoubleCoset.multiplicity Γ₃' Γ₂' Γ₁' δ₂⁻¹ δ₁⁻¹ δ₃⁻¹ — the same coefficient, with the same
caveat about its relation to the Hecke ring's structure constants, as on the form side.
At level Γ₁(N) the single-coset criterion is applied to the upper-triangular representatives
!![1, j; 0, n]: at indices n, m supported on the level (every prime factor dividing N)
they multiply into the representatives at n m, so T_{n m} = T_n T_m on 𝕄_w(Γ₁(N); R)
(heckeTSymbol_mul_of_primeFactors_subset), such operators commute, and T_{n^r} = T_n ^ r.
This is the first piece of the commutativity of the Hecke action on symbols, which the passage
from the period pairing to the integrality of Hecke eigenvalues needs: the transpose of a
composite reverses its order, so the operators being transported must commute among themselves.
Main results #
TauCeti.ModularSymbols.sum_mk_symbolIntRep_eq_nsmul_heckeSymbol_mk: a family of matrices in the double coset meeting each of its right cosetsmtimes sums tom • T_D [x].TauCeti.ModularSymbols.heckeSymbol_heckeSymbol_mkandTauCeti.ModularSymbols.heckeSymbol_heckeSymbol_mk_eq_sum_of_rightCosets: the composite of two Hecke operators on the class ofx, over the chosen and over arbitrary representatives.TauCeti.ModularSymbols.heckeSymbol_comp_heckeSymbol_eq_heckeSymbol: the composite is the operator of a third double coset, when the product set is that coset and the products of the representatives have no right-coset collisions.TauCeti.ModularSymbols.heckeSymbol_comp_heckeSymbol_eq_sum_nsmul: the multiplicity-weighted composition lawT_{D₁} ∘ T_{D₂} = ∑_D m(D₁, D₂; D) • T_D.TauCeti.ModularSymbols.heckeTSymbol_mul_of_primeFactors_subset:T_{n m} = T_n T_mon𝕄_w(Γ₁(N); R)at indices supported on the level, withTauCeti.ModularSymbols.commute_heckeTSymbol_of_primeFactors_subsetandTauCeti.ModularSymbols.heckeTSymbol_pow_of_primeFactors_subset.
References #
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4: the computation preceding Proposition 3.37, and Proposition 3.36 for the upper-triangular representatives.
- W. Stein, Modular Forms: A Computational Approach, Graduate Studies in Mathematics 79, American Mathematical Society, 2007, §8.3.
Families meeting each right coset equally often #
A family meeting each right coset of the double coset m times sums to m times the Hecke
operator. If the matrices aᵢ lie in Γ₁' D.out Γ₂' — so that they are integral,
HeckeRing.GLn.mem_intEntries_of_mem_doubleCoset — and, for every x there, exactly m of them
generate the right coset Γ₁' x, then ∑ᵢ [aᵢ · x] = m • T_D [x].
Covering is not a hypothesis: a right coset named by no member forces m = 0, and then both sides
vanish. This is the shape in which the products aᵢ bⱼ of two families of representatives arrive
once they are grouped by the double coset they lie in.
The composite of two Hecke operators #
The composite of two Hecke operators on the class of x, over the representatives they are
defined with: T_{D₁} (T_{D₂} [x]) = ∑_{v, u} [(aᵥ b_u) · x], the sum over the products of the
chosen right-coset representatives of D₁ and of D₂.
The composite of two Hecke operators, over arbitrary representatives. For any families
(aᵢ), (bⱼ) naming the right cosets of Γ₁' δ₁ Γ₂' and of Γ₂' δ₂ Γ₃' once each — such
matrices are integral, HeckeRing.GLn.mem_intEntries_of_cover —
T_{D₁} (T_{D₂} [x]) = ∑_{i, j} [(aᵢ bⱼ) · x].
This is Shimura's computation in §3.4 on the way to Proposition 3.37, on the symbol side. No
invariance hypothesis appears, in contrast to the slash sums: the classes in the coinvariants are
already invariant, which is what heckeSymbol_mk_eq_sum_of_rightCosets records.
The composite is the Hecke 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: T_{D₁} ∘ T_{D₂} = T_{D₃}.
The hypotheses are those of HeckeRing.GL2.heckeSlashSum_heckeSlashSum_eq_heckeSlashSum: hmul
says that the product set is the single coset D₃, and hinj₃ that the products have no
right-coset collisions. The covering half of what heckeSymbol_mk_eq_sum_of_rightCosets needs is
automatic, by DoubleCoset.doubleCoset_mul_doubleCoset_eq_iUnion_rightCosets, and so is the
integrality of D₃.out: it lies in the product of two double cosets of integral matrices
(HeckeRing.GLn.mem_intEntries_of_mem_doubleCoset_mul_doubleCoset).
The multiplicity-weighted composition law #
The multiplicity-weighted composition law. For double cosets D₁, D₂ of integral
matrices, the composite of the two Hecke operators is the sum, over the double cosets D met by
the products aᵥ b_u of the representatives, of Shimura's multiplicity times the operator of D:
T_{D₁} ∘ T_{D₂} = ∑_D m(D₁, D₂; D) • T_D.
The sum runs over the attached finset of output cosets, each D carrying its membership, from
which mem_intEntries_of_mem_image_pairCoset derives the integrality of D.out that T_D
needs: only the two input cosets are assumed integral, not the monoid Δ.
heckeSymbol_comp_heckeSymbol_eq_heckeSymbol is the special case where the products meet a single
double coset and meet each of its right cosets exactly once. The coefficient is
DoubleCoset.multiplicity Γ₃' Γ₂' Γ₁' δ₂⁻¹ δ₁⁻¹ δ₃⁻¹, exactly as for the slash sums
(HeckeRing.GL2.heckeSlashSum_heckeSlashSum_eq_sum_nsmul), and for the same reason: the sums are
indexed by right cosets.
No finiteness is assumed beyond the two input Hecke triples; the finiteness of each output
coset's own decomposition comes from the composite triple IsHeckeTriple Δ Γ₁' Γ₃', which
IsHeckeTriple.trans derives from the two given ones.
The Hecke operators T_n at indices supported on the level #
The Hecke operators on modular symbols at indices supported on the level multiply:
T_{n m} = T_n ∘ T_m on 𝕄_w(Γ₁(N); R) when every prime factor of n and of m divides N.
At such indices the double coset of diag(1, n) is the union of the n upper-triangular right
cosets Γ₁(N) · !![1, j; 0, n], and HeckeRing.GL2.upperTriRep_mul_upperTriRep matches the pairs
of representatives with the representatives at index n · m bijectively. Nothing here is a
coprimality statement: the identity holds whether or not n and m are coprime.
The Hecke operators on modular symbols at indices supported on the level commute. Both orders compute the operator at the product index.
T_{n^r} = T_n ^ r on modular symbols, at an index supported on the level.