The module of modular symbols #
Let R be a commutative ring, Γ ≤ SL(2, ℤ) a subgroup and w a natural number (the weight is
k = w + 2). The module of modular symbols of weight w + 2 for Γ with coefficients in R
is the module of Γ-coinvariants
𝕄_w(Γ; R) = (Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²))_Γ,
where Div⁰(ℙ¹(ℚ)) is the module of degree-zero R-divisors on the cusps ℙ¹(ℚ) and
Sym^w(R²) is the module of binary forms of degree w. Here SL(2, ℤ) acts on ℙ¹(ℚ) by
Möbius transformations and on binary forms through the inverse of the right action
(P ∣ γ)(X, Y) = P(aX + bY, cX + dY) of TauCeti.binaryFormRep, so that in 𝕄_w(Γ; R) the
modular symbol {α, β} ⊗ P (the class of ([α] - [β]) ⊗ P) satisfies
{γα, γβ} ⊗ P = {α, β} ⊗ (P ∣ γ) for γ ∈ Γ. This is the transformation rule of the period
integral ∫_β^α f(z) P(z, 1) dz of a cusp form f of weight w + 2 on Γ, the relation a
period pairing between cusp forms and modular symbols has to respect.
The main result is that 𝕄_w(Γ; R) is a finitely generated R-module whenever Γ has finite
index. The proof is Manin's: Div⁰(ℙ¹(ℚ)) is spanned by the SL(2, ℤ)-translates of the single
symbol {∞, 0} (because SL(2, ℤ) is generated by S and T and acts transitively on
ℙ¹(ℚ)), and in the coinvariants a translate g{∞, 0} ⊗ P only depends on the coset Γ g up
to changing P. Hence the finitely many symbols r{∞, 0} ⊗ bᵢ, for r running over coset
representatives and bᵢ over a spanning family of the binary forms, span 𝕄_w(Γ; R).
Main definitions #
TauCeti.ModularSymbols.divisorRep R: the permutation representation ofSL(2, ℤ)on theR-divisorsR[ℙ¹(ℚ)]on the cusps.TauCeti.ModularSymbols.degree R: the degree∑ nₓ[x] ↦ ∑ nₓof a cusp divisor.TauCeti.ModularSymbols.degreeZero R: the degree-zero divisorsDiv⁰(ℙ¹(ℚ)), the augmentation submodule of the cusp divisors, equal to the kernel of the degree (degreeZero_eq_ker_degree).TauCeti.ModularSymbols.degreeZeroGLRep R,TauCeti.ModularSymbols.degreeZeroRep R: the representations ofGL(2, ℚ)and ofSL(2, ℤ)onDiv⁰(ℙ¹(ℚ)).TauCeti.ModularSymbols.binaryFormSLRep R w: the left actionP ↦ P ∣ γ⁻¹ofSL(2, ℤ)on binary forms of degreew.TauCeti.ModularSymbols R Γ w: the module of modular symbols𝕄_w(Γ; R).TauCeti.ModularSymbols.symbol Γ α β: the modular symbol{α, β} ⊗ P, as a linear map inP.
Main results #
TauCeti.ModularSymbols.degreeZero_eq_span_unimodular: Manin's lemma,Div⁰(ℙ¹(ℚ))is spanned by the unimodular symbols[g∞] - [g0],g ∈ SL(2, ℤ).TauCeti.ModularSymbols.symbol_mapGL_smul: the relation{γα, γβ} ⊗ P = {α, β} ⊗ (P ∣ γ)forγ ∈ Γ.TauCeti.ModularSymbols.hom_ext_unimodular: a linear map out ofDiv⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²)is determined by its values on the unimodular symbols([g∞] - [g0]) ⊗ P.TauCeti.ModularSymbols.span_symbol_eq_top: the symbols{α, β} ⊗ Pspan the module.TauCeti.ModularSymbols.instModuleFinite:𝕄_w(Γ; R)is a finiteR-module whenΓhas finite index inSL(2, ℤ);TauCeti.ModularSymbols.instModuleFiniteIntis the integral case.
References #
- Y. I. Manin, Parabolic points and zeta functions of modular curves, Izv. Akad. Nauk SSSR Ser. Mat. 36 (1972), 19–66, §1.
- W. Stein, Modular Forms: A Computational Approach, Graduate Studies in Mathematics 79, American Mathematical Society, 2007, §8.2 and Proposition 8.3.
Divisors on the cusps #
The degree ∑ nₓ[x] ↦ ∑ nₓ of an R-divisor on the cusps, the coefficient sum.
Equations
Instances For
The degree-zero divisors Div⁰(ℙ¹(ℚ)) on the cusps: the augmentation submodule of the
R-divisors R[ℙ¹(ℚ)], that is, the kernel of the degree map TauCeti.ModularSymbols.degree
(see TauCeti.ModularSymbols.degreeZero_eq_ker_degree).
Equations
Instances For
The permutation representation of SL(2, ℤ) on the R-divisors R[ℙ¹(ℚ)] on the cusps
ℙ¹(ℚ) = OnePoint ℚ, through the Möbius action of GL(2, ℚ).
Equations
Instances For
The representation of GL(2, ℚ) on the degree-zero divisors Div⁰(ℙ¹(ℚ)), through the
Möbius action on the cusps. Its restriction to SL(2, ℤ) is TauCeti.ModularSymbols.degreeZeroRep;
the larger group is what the Hecke operators on modular symbols act through.
Equations
Instances For
The representation of SL(2, ℤ) on the degree-zero divisors Div⁰(ℙ¹(ℚ)).
Equations
Instances For
The SL(2, ℤ)-representation on Div⁰(ℙ¹(ℚ)) is the GL(2, ℚ)-representation along
mapGL ℚ.
On the underlying divisor, degreeZeroRep is the permutation representation divisorRep.
Not @[simp]: simp normalises degreeZeroRep R g to degreeZeroGLRep R (mapGL ℚ g) through
degreeZeroRep_apply, and this lemma is the bridge to divisorRep for rw.
The divisor [α] - [β] has degree zero.
A GL(2, ℚ) translate of [α] - [β] is the difference of the translated cusps.
Manin's lemma. The degree-zero divisors on the cusps are spanned by the unimodular
symbols [g∞] - [g0], g ∈ SL(2, ℤ), that is, by the SL(2, ℤ)-translates of [∞] - [0].
Manin's lemma, inside Div⁰(ℙ¹(ℚ)): the SL(2, ℤ)-translates of [∞] - [0] span the
degree-zero divisors.
Binary forms as a left representation #
The left action P ↦ P ∣ γ⁻¹ of SL(2, ℤ) on binary forms of degree w, obtained from the
right action (P ∣ γ)(X, Y) = P(aX + bY, cX + dY) of TauCeti.binaryFormRep.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The left action undoes the right action: (P ∣ γ) ∣ γ⁻¹ = P.
The right action undoes the left action: (P ∣ γ⁻¹) ∣ γ = P. Not @[simp]: simp first
rewrites the inner binaryFormSLRep R w γ P to the adjugate action.
On SL(2, ℤ) the adjugate action TauCeti.binaryFormAdjugateRep on binary forms is the
action P ↦ P ∣ γ⁻¹ defining the modular symbols: the adjugate of a determinant-one matrix is its
inverse.
The diagonal representation of SL(2, ℤ) on Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²).
Equations
Instances For
Two linear maps out of Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²) are equal as soon as they agree on the
unimodular symbols ([g∞] - [g0]) ⊗ P, g ∈ SL(2, ℤ), which span by Manin's lemma
(TauCeti.ModularSymbols.span_degreeZeroRep_eq_top).
The module of modular symbols 𝕄_w(Γ; R) = (Div⁰(ℙ¹(ℚ)) ⊗_R Sym^w(R²))_Γ of weight
w + 2 for a subgroup Γ ≤ SL(2, ℤ), with coefficients in R: the Γ-coinvariants of the
degree-zero divisors on the cusps tensored with the binary forms of degree w.
This is an abbreviation for the coinvariants, so that their universal property
(Representation.Coinvariants.lift, Representation.Coinvariants.hom_ext) applies directly.
Equations
Instances For
The modular symbol {α, β} ⊗ P ∈ 𝕄_w(Γ; R), the class of ([α] - [β]) ⊗ P, as an R-linear
map in the binary form P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Γ-relation. For γ ∈ Γ, {γα, γβ} ⊗ P = {α, β} ⊗ (P ∣ γ).
The classes of the translates g([∞] - [0]) ⊗ P span 𝕄_w(Γ; R).
The modular symbols {α, β} ⊗ P span 𝕄_w(Γ; R).
Finiteness of modular symbols. For a subgroup Γ of finite index in SL(2, ℤ), the
module of modular symbols 𝕄_w(Γ; R) is a finitely generated R-module.
Finiteness of integral modular symbols. For a subgroup Γ of finite index in SL(2, ℤ),
𝕄_w(Γ; ℤ) is a finitely generated abelian group.
This is instModuleFinite at R = ℤ, restated because instance search equips 𝕄_w(Γ; ℤ) with
the ℤ-module structure AddCommGroup.toIntModule of its additive group, which is equal but not
reducibly defeq to the module structure of the coinvariants.