The period polynomial of a level-one cusp form

Let f be a cusp form of weight k = w + 2 on SL(2, ℤ). Its period polynomial is the binary form of degree w

r_f(X, Y) = ∫₀^{i∞} f(τ) (X - τY)ʷ dτ,

whose coefficients are, up to binomial coefficients and signs, the periods ∫₀^{i∞} f(τ) τʲ dτ, 0 ≤ j ≤ w. Here it is built from the period map on modular symbols of level one: the functional P ↦ ∫₀^{i∞} f(τ) P(τ, 1) dτ on binary forms is the period map of f evaluated on the symbols {∞, 0} ⊗ P, and r_f is the binary form attached to this functional by TauCeti.binaryFormDual.

The relations among modular symbols become relations among period polynomials. Since the period map of f sends the symbol {g∞, g0} ⊗ P to the period of P ∣ g, the two-term and three-term Manin relations say that r_f is killed by 1 + S and by 1 + U + U²: the period polynomial lies in the period-polynomial space W_w. Since the symbols {g∞, g0} ⊗ P span the modular symbols, r_f determines all the periods of f, so the injectivity of the period map makes f ↦ r_f injective. This is the map S_k(SL(2, ℤ)) → W_w of the Eichler–Shimura theory, and TauCeti.periodPolynomial is stated with codomain W_w.

Its even and odd parts r_f^± = (r_f(X, Y) ± r_f(-X, Y)) / 2, the components of r_f in the eigenspaces W_w^± of the parity involution P(X, Y) ↦ P(-X, Y), are the even and odd period polynomials of f. Together with the dimension count dim W_w = dim M_k + dim S_k of TauCeti.NumberTheory.ModularForms.LevelOne.PeriodPolynomial.Finrank, they are what compare W_w with the spaces of modular forms in the period-polynomial approach to the Eichler–Selberg trace formula.

Main definitions

• TauCeti.periodPolynomial hk: the ℂ-linear map f ↦ r_f from cusp forms of weight k = w + 2 on SL(2, ℤ) to the period-polynomial space W_w.
• TauCeti.evenPeriodPolynomial hk, TauCeti.oddPeriodPolynomial hk: the ℂ-linear maps f ↦ r_f^± to the even and odd period polynomials W_w^±.

Main results

• TauCeti.eval_periodPolynomial: r_f(x, y) = ∫₀^{i∞} f(τ) (x - τy)ʷ dτ.
• TauCeti.coe_periodPolynomial_eq_binaryFormDual: r_f is the binary form attached to the period map of f on the symbols {∞, 0} ⊗ P.
• TauCeti.periodPolynomial_injective: f ↦ r_f is injective.
• TauCeti.coe_evenPeriodPolynomial_add_coe_oddPeriodPolynomial: r_f = r_f^+ + r_f^-.
• TauCeti.binaryFormMonomialBasis_repr_evenPeriodPolynomial, TauCeti.binaryFormMonomialBasis_repr_oddPeriodPolynomial: the coordinates of r_f^+ and r_f^- in the monomial basis are those of r_f at even and at odd exponents of X.

References

• W. Kohnen and D. Zagier, Modular forms with rational periods, in Modular Forms (R. A. Rankin, ed.), Ellis Horwood, 1984, 197–249, §1.
• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, arXiv:1711.00327, §2.
• Y. I. Manin, Periods of parabolic forms and p-adic Hecke series, Mat. Sb. 92 (1973), 378–401, §1.

noncomputable def TauCeti.periodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k →ₗ[ℂ] ↥(periodPolynomials ℂ w)

The period polynomial r_f(X, Y) = ∫₀^{i∞} f(τ) (X - τY)ʷ dτ of a cusp form f of weight k = w + 2 on SL(2, ℤ) (TauCeti.eval_periodPolynomial), as a ℂ-linear map to the period-polynomial space W_w. It is the binary form attached by TauCeti.binaryFormDual to the functional P ↦ ∫₀^{i∞} f(τ) P(τ, 1) dτ, the period map of f on the modular symbols {∞, 0} ⊗ P; it lies in W_w because of the two-term and three-term Manin relations.

theorem TauCeti.coe_periodPolynomial_eq_binaryFormDual {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) {F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) ⊤) k} (hF : ⇑F = ⇑f) : ↑((periodPolynomial hk) f) = (binaryFormDual ℂ w) ((ModularSymbols.periodMap ℂ ⊤ hk) F ∘ₗ ModularSymbols.symbol ⊤ OnePoint.infty ↑0)

The period polynomial through the period map. For a cusp form F for the image of ⊤ : Subgroup SL(2, ℤ) with the same underlying function as f, the period polynomial r_f is the binary form attached by TauCeti.binaryFormDual to the functional P ↦ ⟪F, {∞, 0} ⊗ P⟫ of the period map.

@[simp]

theorem TauCeti.eval_periodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (x y : ℂ) : (MvPolynomial.eval ![x, y]) ↑↑((periodPolynomial hk) f) = cuspIntegral (fun (τ : UpperHalfPlane) => f τ * (x - ↑τ * y) ^ w) (↑0) OnePoint.infty

The values of the period polynomial: r_f(x, y) = ∫₀^{i∞} f(τ) (x - τy)ʷ dτ.

theorem TauCeti.periodPolynomial_injective {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : Function.Injective ⇑(periodPolynomial hk)

The period polynomial determines the cusp form: f ↦ r_f is injective.

The even and odd period polynomials

noncomputable def TauCeti.evenPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k →ₗ[ℂ] ↥(evenPeriodPolynomials ℂ w)

The even period polynomial r_f^+(X, Y) = (r_f(X, Y) + r_f(-X, Y)) / 2 of a cusp form f of weight k = w + 2 on SL(2, ℤ), as a ℂ-linear map to the even period polynomials W_w^+.

noncomputable def TauCeti.oddPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k →ₗ[ℂ] ↥(oddPeriodPolynomials ℂ w)

The odd period polynomial r_f^-(X, Y) = (r_f(X, Y) - r_f(-X, Y)) / 2 of a cusp form f of weight k = w + 2 on SL(2, ℤ), as a ℂ-linear map to the odd period polynomials W_w^-.

theorem TauCeti.coe_evenPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ↑((evenPeriodPolynomial hk) f) = 2⁻¹ • (↑((periodPolynomial hk) f) + ((binaryFormRep ℂ w) (MulOpposite.op !![-1, 0; 0, 1])) ↑((periodPolynomial hk) f))

The even period polynomial is r_f^+ = (r_f + r_f ∣ ε) / 2, with ε = !![-1, 0; 0, 1].

theorem TauCeti.coe_oddPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ↑((oddPeriodPolynomial hk) f) = 2⁻¹ • (↑((periodPolynomial hk) f) - ((binaryFormRep ℂ w) (MulOpposite.op !![-1, 0; 0, 1])) ↑((periodPolynomial hk) f))

The odd period polynomial is r_f^- = (r_f - r_f ∣ ε) / 2, with ε = !![-1, 0; 0, 1].

theorem TauCeti.coe_evenPeriodPolynomial_add_coe_oddPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ↑((evenPeriodPolynomial hk) f) + ↑((oddPeriodPolynomial hk) f) = ↑((periodPolynomial hk) f)

The period polynomial is the sum of its even and odd parts: r_f = r_f^+ + r_f^-.

theorem TauCeti.binaryFormMonomialBasis_repr_evenPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (j : Fin (w + 1)) : ((binaryFormMonomialBasis ℂ w).repr ↑((evenPeriodPolynomial hk) f)) j = if Even ↑j then ((binaryFormMonomialBasis ℂ w).repr ↑((periodPolynomial hk) f)) j else 0

The coordinates of the even period polynomial r_f^+ in the monomial basis Xʲ Yʷ⁻ʲ: those of r_f at even j, and 0 at odd j.

theorem TauCeti.binaryFormMonomialBasis_repr_oddPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (j : Fin (w + 1)) : ((binaryFormMonomialBasis ℂ w).repr ↑((oddPeriodPolynomial hk) f)) j = if Even ↑j then 0 else ((binaryFormMonomialBasis ℂ w).repr ↑((periodPolynomial hk) f)) j

The coordinates of the odd period polynomial r_f^- in the monomial basis Xʲ Yʷ⁻ʲ: those of r_f at odd j, and 0 at even j.