The period map

Let Γ ≤ SL(2, ℤ) be a subgroup of finite index, R a commutative ring with an algebra map to ℂ (typically ℤ), and f a cusp form of weight k = w + 2 on Γ. The raw period pairing TauCeti.ModularSymbols.rawPairing R f sends ([α] - [β]) ⊗ P in Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²) to the period ∫_β^α f(z) P(z, 1) dz. This file shows that it is invariant under the diagonal action of Γ, and hence descends to the module of modular symbols 𝕄_w(Γ; R), the Γ-coinvariants. The invariance is the substitution z ↦ γz in the period integral together with the slash invariance f ∣[k] γ = f for γ ∈ Γ (TauCeti.ModularSymbols.cuspIntegral_periodIntegrand_mapGL_smul_of_mem).

The descended functionals are ℂ-linear in f, so they assemble into the period map S_k(Γ) →ₗ[ℂ] (𝕄_w(Γ; R) →ₗ[R] ℂ). It sends a cusp form to an R-linear functional on the modular symbols, rather than a form to a symbol: symbols are cycles and forms are integrated over them, so for R = ℤ the integral structure stays on the source of the functionals. On the symbol {α, β} ⊗ P the functional of f is the period ∫_β^α f(z) P(z, 1) dz.

Main definitions

• TauCeti.ModularSymbols.periodMap R Γ hk: the period map S_k(Γ) →ₗ[ℂ] (𝕄_w(Γ; R) →ₗ[R] ℂ), for k = w + 2.

Main results

• TauCeti.ModularSymbols.rawPairing_comp_symbolRep: the raw pairing of a cusp form on Γ is invariant under the diagonal action of Γ on Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²).
• TauCeti.ModularSymbols.periodMap_mk: on the class of x, the functional of f is the raw pairing of f with x.
• TauCeti.ModularSymbols.periodMap_symbol: on the symbol {α, β} ⊗ P, the functional of f is the period ∫_β^α f(z) P(z, 1) dz.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §8.2, (8.2.15)–(8.2.16).
• 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.5.

theorem TauCeti.ModularSymbols.rawPairing_comp_symbolRep {R : Type u_1} [CommRing R] [Algebra R ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {w : ℕ} {F : Type u_2} [FunLike F UpperHalfPlane ℂ] [CuspFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hk : k = ↑w + 2) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ Γ) : rawPairing R f hk ∘ₗ (symbolRep R w) γ = rawPairing R f hk

Invariance of the raw pairing. For a cusp form f of weight w + 2 on Γ and γ ∈ Γ, the raw pairing of f is invariant under the diagonal action of γ on Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²): ⟪f, {γα, γβ} ⊗ (P ∣ γ⁻¹)⟫ = ⟪f, {α, β} ⊗ P⟫.

noncomputable def TauCeti.ModularSymbols.periodMap (R : Type u_1) [CommRing R] [Algebra R ℂ] (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) [Γ.FiniteIndex] {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k →ₗ[ℂ] ModularSymbols R Γ w →ₗ[R] ℂ

The period map S_k(Γ) →ₗ[ℂ] (𝕄_w(Γ; R) →ₗ[R] ℂ) for k = w + 2: a cusp form f on Γ is sent to the R-linear functional on the modular symbols induced by its raw period pairing, so that {α, β} ⊗ P ↦ ∫_β^α f(z) P(z, 1) dz. For R = ℤ this is the pairing of cusp forms with the integral modular symbols.

Equations

• TauCeti.ModularSymbols.periodMap R Γ hk = { toFun := TauCeti.ModularSymbols.periodFunctional✝ hk, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ModularSymbols.periodMap_mk {R : Type u_1} [CommRing R] [Algebra R ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (x : TensorProduct R ↥(degreeZero R) ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : ((periodMap R Γ hk) f) ((Representation.Coinvariants.mk (MonoidHom.comp (symbolRep R w) Γ.subtype)) x) = (rawPairing R f hk) x

On the class of x ∈ Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²), the period map is the raw pairing.

theorem TauCeti.ModularSymbols.periodMap_symbol {R : Type u_1} [CommRing R] [Algebra R ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k) (α β : OnePoint ℚ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : ((periodMap R Γ hk) f) ((symbol Γ α β) P) = cuspIntegral (periodIntegrand (⇑f) P) β α

On the symbol {α, β} ⊗ P, the period map is the period ∫_β^α f(z) P(z, 1) dz.