Hecke operators on modular symbols #
An integral matrix δ ∈ GL(2, ℚ) acts on Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²) by
δ · ({α, β} ⊗ P) = {δα, δβ} ⊗ (P ∣ adj δ),
the Möbius action on the cusps tensored with the adjugate action TauCeti.binaryFormAdjugateRep
on binary forms (TauCeti.ModularSymbols.symbolIntRep). On SL(2, ℤ) the adjugate is the
inverse, so this extends the action TauCeti.ModularSymbols.symbolRep through which the module
of modular symbols 𝕄_w(Γ; R) is defined as coinvariants. It is the action adjoint to Mathlib's
weight-w + 2 slash action under the period pairing
∫_β^α f(z) P(z, 1) dz: substituting z ↦ δz gives
⟪f ∣[k] δ, {α, β} ⊗ P⟫ = ⟪f, δ · ({α, β} ⊗ P)⟫ with no determinant factor.
For a double coset D = Γ₁' δ Γ₂' of a Hecke triple in GL(2, ℚ) whose flanks are the images
Γᵢ' = Γᵢ.map (mapGL ℚ) of subgroups Γ₁, Γ₂ ≤ SL(2, ℤ), decomposed into right cosets
Γ₁' δ Γ₂' = ⊔ᵥ Γ₁' aᵥ, the Hecke operator on modular symbols is
T_D : 𝕄_w(Γ₂; R) → 𝕄_w(Γ₁; R), {α, β} ⊗ P ↦ ∑ᵥ {aᵥα, aᵥβ} ⊗ (P ∣ adj aᵥ)
(TauCeti.ModularSymbols.heckeSymbol). It is well defined because right multiplication by
Γ₂' permutes the right cosets (HeckeCoset.heckeSum_comp_of_mem), and it is independent of
the representatives chosen (heckeSymbol_symbol_eq_sum_of_rightCosets). Taking Γ₁ = Γ₂ = Γ₁(N)
and the double coset of diag(1, n) gives the Hecke operator T_n on 𝕄_w(Γ₁(N); R)
(TauCeti.ModularSymbols.heckeTSymbol), the operator of the same double coset as T_n on
modular forms. Over R = ℤ these are endomorphisms of a finitely generated abelian group, which
is the integrality of the Hecke action that makes the Hecke eigenvalues of cusp forms algebraic
integers once the period pairing is shown to be Hecke-equivariant and injective.
Main definitions #
TauCeti.ModularSymbols.symbolIntRep R w: the action of the integral matricesintEntries 2onDiv⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²), extendingTauCeti.ModularSymbols.symbolRep.TauCeti.ModularSymbols.heckeSymbol Γ₁ Γ₂ D hD: the Hecke operator𝕄_w(Γ₂; R) →ₗ[R] 𝕄_w(Γ₁; R)of a double cosetDwhose representativeD.outis an integral matrix.TauCeti.ModularSymbols.heckeTSymbol N n: the Hecke operatorT_non𝕄_w(Γ₁(N); R).
Main results #
TauCeti.ModularSymbols.symbolIntRep_mapGL: onSL(2, ℤ)the action issymbolRep, andTauCeti.ModularSymbols.mk_symbolIntRep_eq_of_rightCoset_eq: the class ofδ · xin𝕄_w(Γ₁; R)depends only on the right cosetΓ₁' δ.TauCeti.ModularSymbols.heckeSymbol_symbol: the formulaT_D ({α, β} ⊗ P) = ∑ᵥ {aᵥα, aᵥβ} ⊗ (P ∣ adj aᵥ)over the chosen representatives, andTauCeti.ModularSymbols.heckeSymbol_symbol_eq_sum_of_rightCosets, the same formula over any family of representatives of the right cosets.TauCeti.ModularSymbols.heckeSymbol_one: the identity double coset acts as the identity, andTauCeti.ModularSymbols.heckeTSymbol_one:T₁ = 1.TauCeti.ModularSymbols.heckeTSymbol_congr:T_ntransported along an equality of indices, each carrying its ownNeZeroinstance.
References #
- Y. I. Manin, Parabolic points and zeta functions of modular curves, Izv. Akad. Nauk SSSR Ser. Mat. 36 (1972), 19–66, §2.
- W. Stein, Modular Forms: A Computational Approach, Graduate Studies in Mathematics 79, American Mathematical Society, 2007, §8.3.
- G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4 and §8.2.
The action of integral matrices on Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²) #
The action of integral matrices on Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²):
δ · (D ⊗ P) = δD ⊗ (P ∣ adj δ), the Möbius action on the cusps tensored with the adjugate
action on binary forms, as a representation of the monoid intEntries 2 of invertible integral
matrices. On SL(2, ℤ) it is TauCeti.ModularSymbols.symbolRep (symbolIntRep_mapGL).
Equations
- One or more equations did not get rendered due to their size.
Instances For
On SL(2, ℤ) the action of integral matrices is the action symbolRep defining the modular
symbols.
The class of δ · (([α] - [β]) ⊗ P) in 𝕄_w(Γ; R) is the symbol
{δα, δβ} ⊗ (P ∣ adj δ).
The Hecke operator of a double coset #
The projection onto 𝕄_w(Γ₁; R) is invariant under the action of Γ₁.map (mapGL ℚ)
through symbolIntRep: that action is symbolRep, which the coinvariants kill.
The class of δ · x in 𝕄_w(Γ₁; R) depends only on the right coset Γ₁' δ. If
Γ₁' δ₁ = Γ₁' δ₂ then δ₂ = (δ₂ δ₁⁻¹) δ₁ with δ₂ δ₁⁻¹ ∈ Γ₁' — so δ₂ is integral along with
δ₁ (HeckeRing.GLn.mem_intEntries_of_rightCoset_eq) — and the coinvariants do not see that
factor.
The enumeration ∑ needs, obtained from the Finite assumption by choice exactly as in
HeckeRing/Representation.lean, so that the sums below are the terms heckeSum_apply produces.
It is local and noncomputable: no declaration in this file depends on which enumeration is
chosen.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Hecke operator of a double coset on modular symbols. For D = Γ₁' δ Γ₂' = ⊔ᵥ Γ₁' aᵥ
with Γᵢ' = Γᵢ.map (mapGL ℚ), this is the R-linear map 𝕄_w(Γ₂; R) → 𝕄_w(Γ₁; R) sending
{α, β} ⊗ P to ∑ᵥ {aᵥα, aᵥβ} ⊗ (P ∣ adj aᵥ) (heckeSymbol_symbol). It is the descent to the
Γ₂-coinvariants of the Hecke sum HeckeCoset.heckeSum of D on symbolIntRep, and it depends
on the double coset alone, not on the representatives (heckeSymbol_symbol_eq_sum_of_rightCosets).
The hypothesis hD is what lets the representatives act integrally: the chosen D.out is an
integral matrix, and Γ₂ consists of them, so every representative does
(DoubleCoset.rightCosetRep_mem). Nothing is asked of the rest of Δ; for the double cosets of
the modular-forms theory the hypothesis is supplied by Delta0_le_intEntries.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On the class of x, the Hecke operator is the Hecke sum HeckeCoset.heckeSum of the double
coset on symbolIntRep, relative to the projection onto 𝕄_w(Γ₁; R): the defining equation of
heckeSymbol, which is a lift out of the coinvariants.
The Hecke operator on the class of x ∈ Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²): the sum of the classes of
the translates aᵥ · x over the chosen right-coset representatives.
The Hecke operator on a modular symbol, over the chosen representatives:
T_D ({α, β} ⊗ P) = ∑ᵥ {aᵥα, aᵥβ} ⊗ (P ∣ adj aᵥ).
The Hecke operator on the class of x, over any family of representatives of the right
cosets. If the right cosets Γ₁' aᵢ are pairwise distinct and cover Γ₁' D.out Γ₂', and each
aᵢ is the cast of the integral matrix Aᵢ, then T_D [x] = ∑ᵢ [aᵢ · x].
The Hecke operator on a modular symbol, over any family of representatives of the right
cosets. If the right cosets Γ₁' aᵢ are pairwise distinct and cover Γ₁' D.out Γ₂', and
aᵢ is the cast of the integral matrix Aᵢ, then
T_D ({α, β} ⊗ P) = ∑ᵢ {aᵢα, aᵢβ} ⊗ (P ∣ adj Aᵢ). This is the form in which explicit coset
representatives — say the matrices !![1, j; 0, p] and !![p, 0; 0, 1] for T_p — are read
off.
The identity double coset acts as the identity on 𝕄_w(Γ; R): Γ' · 1 · Γ' = Γ' is a
single right coset, represented by 1.
The Hecke operators T_n at level Γ₁(N) #
The Hecke operator T_n on 𝕄_w(Γ₁(N); R): the operator of the double coset
Γ₁(N) · diag(1, n) · Γ₁(N), the same double coset that defines T_n on modular forms of level
Γ₁(N) (HeckeRing.GL2.heckeTNat). The NeZero n binder records that Hecke operators are indexed
by positive integers; at n = 0 the double coset would degenerate to Γ₁(N) itself. As for
heckeTNat, the binder is _-named because only the statements use it: the body is the same
operator either way, and it is the index that is being constrained.
Equations
Instances For
The defining equation of heckeTSymbol.