The raw period pairing

Let f be a cusp form of weight w + 2 and R a commutative ring with an algebra map to ℂ (typically ℤ). The raw period pairing of f sends a degree-zero R-divisor on the rational cusps, tensored with a homogeneous binary form P of degree w with coefficients in R, to the corresponding period of f. On the generators it is

([α] - [β]) ⊗ P ↦ ∫_β^α f(z) P(z, 1) dz.

The construction first pairs a divisor with the cusp values ∫_∞^α f(z) P(z, 1) dz. Additivity of periods shows that the difference of two such values is the integral from β to α. This produces an R-bilinear pairing on Div⁰(ℙ¹(ℚ)) × Sym^w(R²), which is then lifted through the tensor product. The pairing is ℂ-linear in f. Its invariance under the diagonal modular-group action and its descent to modular symbols are in TauCeti.NumberTheory.ModularForms.ModularSymbols.Period.Map.

Main definitions

• TauCeti.ModularSymbols.rawPairing: the raw period functional on Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²).

Main results

• TauCeti.ModularSymbols.rawPairing_single_sub_single_tmul: the raw pairing sends ([α] - [β]) ⊗ P to ∫_β^α f(z) P(z, 1) dz.
• TauCeti.ModularSymbols.rawPairing_add, TauCeti.ModularSymbols.rawPairing_smul: the raw pairing is ℂ-linear in the cusp form.

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.

noncomputable def TauCeti.ModularSymbols.rawPairing (R : Type u_1) [CommRing R] [Algebra R ℂ] {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} {w : ℕ} {F : Type u_2} [hF : FunLike F UpperHalfPlane ℂ] [CuspFormClass F 𝒢 k] (f : F) (hk : k = ↑w + 2) : TensorProduct R ↥(degreeZero R) ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] ℂ

The raw period pairing of a cusp form of weight w + 2. It is the R-linear functional on Div⁰(ℙ¹(ℚ)) ⊗ Sym^w(R²) induced by integrating against binary forms.

Equations

• TauCeti.ModularSymbols.rawPairing R f hk = TensorProduct.lift (TauCeti.ModularSymbols.periodDivisorPairing✝ R f hk)

theorem TauCeti.ModularSymbols.rawPairing_tmul {R : Type u_1} [CommRing R] [Algebra R ℂ] {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} {w : ℕ} {F : Type u_2} [hF : FunLike F UpperHalfPlane ℂ] [CuspFormClass F 𝒢 k] (f : F) (hk : k = ↑w + 2) (D : ↥(degreeZero R)) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (rawPairing R f hk) (D ⊗ₜ[R] P) = (Finsupp.linearCombination R fun (α : OnePoint ℚ) => cuspIntegral (periodIntegrand (⇑f) P) OnePoint.infty α) (↑D).coeff

On a pure tensor, the raw pairing is the coefficient-weighted sum of periods from ∞ to the cusps in the divisor.

@[simp]

theorem TauCeti.ModularSymbols.rawPairing_single_sub_single_tmul {R : Type u_1} [CommRing R] [Algebra R ℂ] {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} {w : ℕ} {F : Type u_2} [hF : FunLike F UpperHalfPlane ℂ] [CuspFormClass F 𝒢 k] (f : F) (hk : k = ↑w + 2) (α β : OnePoint ℚ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (rawPairing R f hk) (⟨MonoidAlgebra.single α 1 - MonoidAlgebra.single β 1, ⋯⟩ ⊗ₜ[R] P) = cuspIntegral (periodIntegrand (⇑f) P) β α

The raw pairing sends ([α] - [β]) ⊗ P to the period from β to α. This is the characteristic formula relating the analytic pairing to the generators of modular symbols.

theorem TauCeti.ModularSymbols.rawPairing_add {R : Type u_1} [CommRing R] [Algebra R ℂ] {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} {w : ℕ} (f g : CuspForm 𝒢 k) (hk : k = ↑w + 2) : rawPairing R (f + g) hk = rawPairing R f hk + rawPairing R g hk

The raw pairing is additive in the cusp form.

theorem TauCeti.ModularSymbols.rawPairing_smul {R : Type u_1} [CommRing R] [Algebra R ℂ] {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.IsArithmetic] {k : ℤ} {w : ℕ} [𝒢.HasDetOne] (c : ℂ) (f : CuspForm 𝒢 k) (hk : k = ↑w + 2) : rawPairing R (c • f) hk = c • rawPairing R f hk

The raw pairing is ℂ-homogeneous in the cusp form.