The Eichler–Shimura period-polynomial isomorphism at level one

Let k = w + 2 be an integer weight with w : ℕ. For a cusp form f ∈ S_k(SL(2, ℤ)), its even and odd period polynomials r_f^+ ∈ W_w^+ and r_f^- ∈ W_w^- collect the critical L-values of f of the two parities (TauCeti.evenPeriodPolynomial, TauCeti.oddPeriodPolynomial). This file proves that at level one:

1. Injectivity on cusp forms. Both evenPeriodPolynomial hk and oddPeriodPolynomial hk are injective (evenPeriodPolynomial_injective, oddPeriodPolynomial_injective). For odd w, S_{w+2}(SL(2, ℤ)) = 0 (CuspForm.levelOne_odd_weight_eq_zero). For even w, the kernel of each map is stable under every prime Hecke operator T_p because PeriodRelation ℂ p has a solution (exists_periodRelation) that intertwines T_p with periodAction (PeriodRelation.periodAction_evenPeriodPolynomial, PeriodRelation.periodAction_oddPeriodPolynomial). By injective_of_heckeTCuspLevelOne_mem_ker, injectivity reduces to nonvanishing on levelOneNewformBasis k: any level-one newform f forces k ≥ 12 (w ≥ 10), where s = w and s = w + 1 lie strictly inside the Euler-product half-plane Re s > k/2 + 1 where L(f, s) ≠ 0.
2. The odd Eichler–Shimura isomorphism. Since dim W_w^- = dim S_{w+2}(SL(2, ℤ)) (finrank_oddPeriodPolynomials_eq_finrank_cuspForm), oddPeriodPolynomial hk upgrades to a Hecke-equivariant linear equivalence oddPeriodPolynomialEquiv hk : CuspForm 𝒮ℒ k ≃ₗ[ℂ] W_w^-.
3. Disjointness of X^w - Y^w and the even Eichler–Shimura isomorphism. Since every solution ξ of PeriodRelation R n ξ (n ≥ 1) scales the Eisenstein period polynomial X^w - Y^w by σ_{w+1}(n) (PeriodRelation.periodAction_eisensteinPeriodPolynomial), a cusp form whose even period polynomial were X^w - Y^w would be a nonzero cusp form with Hecke eigenvalues σ_{w+1}(n), contradicting the absolute convergence of its Dirichlet series at s = w + 1 for w ≥ 10. Hence W_w^+ is the internal direct sum of range (evenPeriodPolynomial hk) and ℂ · (X^w - Y^w) for positive even w, giving a Hecke-equivariant linear equivalence extendedEvenPeriodPolynomialEquiv hk : ModularForm 𝒮ℒ k ≃ₗ[ℂ] W_w^+ and the full Eichler–Shimura isomorphism periodPolynomialEquiv hk : (ModularForm 𝒮ℒ k × CuspForm 𝒮ℒ k) ≃ₗ[ℂ] W_w.
4. Trace identity for the Eichler–Selberg trace formula. Conjugating along periodPolynomialEquiv hk identifies the trace on W_w of any element ξ satisfying both the period relation (A) and the exchange relations (B) — in particular Popa–Zagier's explicit element popaZagierElement ℂ n — with 2 Tr(Tₙ | S_k) + σ_{w+1}(n). Combined with Popa–Zagier's trace reduction Tr(ξ | W_w) = Tr(ξ | V_w) (ExchangeRelations.trace_periodActionRestrict_eq_trace), this expresses Tr(Tₙ | S_k) directly in terms of the binary-form trace Tr(ξ | V_w).

Main definitions

• TauCeti.oddPeriodPolynomialEquiv: the ℂ-linear isomorphism CuspForm 𝒮ℒ k ≃ₗ[ℂ] W_w^-.
• TauCeti.extendedEvenPeriodPolynomialEquiv: the ℂ-linear isomorphism ModularForm 𝒮ℒ k ≃ₗ[ℂ] W_w^+ extending evenPeriodPolynomial hk and sending ModularForm.E to X^w - Y^w in positive even degree.
• TauCeti.periodPolynomialEquiv: the full ℂ-linear Eichler–Shimura isomorphism (ModularForm 𝒮ℒ k × CuspForm 𝒮ℒ k) ≃ₗ[ℂ] W_w.

Main results

• TauCeti.evenPeriodPolynomial_injective, TauCeti.oddPeriodPolynomial_injective: injectivity of the even and odd period maps on CuspForm 𝒮ℒ k.
• TauCeti.isCompl_range_evenPeriodPolynomial_span_eisensteinPeriodPolynomial: for positive even w, W_w^+ = r^+(S_k) ⊕ ℂ · (X^w - Y^w).
• TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_extendedEvenPeriodPolynomialEquiv: Hecke equivariance of extendedEvenPeriodPolynomialEquiv.
• TauCeti.TraceFormulaMatrixModule.PeriodRelation.trace_periodAction_eq, TauCeti.TraceFormulaMatrixModule.trace_heckeTCuspLevelOne_eq_trace_popaZagierElement: reduction of Tr(Tₙ | S_k) to the ambient binary-form trace of popaZagierElement ℂ n on V_w.

References

• M. Eichler, Eine Verallgemeinerung der Abelschen Integrale, Math. Z. 67 (1957), 267–298.
• G. Shimura, Sur les intégrales attachées aux formes automorphes, J. Math. Soc. Japan 11 (1959), 291–311.
• Y. I. Manin, Periods of parabolic forms and p-adic Hecke series, Mat. Sb. 92 (1973), 378–401.
• W. Kohnen and D. Zagier, Modular forms with rational periods, in Modular Forms (R. A. Rankin, ed.), Ellis Horwood, 1984, 197–249, §1.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, Propositions 2 and 3.

Nonvanishing on level-one newforms and injectivity of r_f^+ and r_f^-

theorem TauCeti.evenPeriodPolynomial_levelOneNewformBasis_ne_zero {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : HeckeRing.GL2.Newform 1 k) : (evenPeriodPolynomial hk) ((levelOneNewformBasis k) f) ≠ 0

The even period polynomial of a level-one newform is nonzero.

theorem TauCeti.oddPeriodPolynomial_levelOneNewformBasis_ne_zero {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (f : HeckeRing.GL2.Newform 1 k) : (oddPeriodPolynomial hk) ((levelOneNewformBasis k) f) ≠ 0

The odd period polynomial of a level-one newform is nonzero.

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

The even period-polynomial map is injective on CuspForm 𝒮ℒ k at every degree w.

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

The odd period-polynomial map is injective on CuspForm 𝒮ℒ k at every degree w.

The odd Eichler–Shimura isomorphism CuspForm 𝒮ℒ k ≃ₗ[ℂ] oddPeriodPolynomials ℂ w

theorem TauCeti.oddPeriodPolynomial_surjective {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : Function.Surjective ⇑(oddPeriodPolynomial hk)

The odd period-polynomial map is surjective onto oddPeriodPolynomials ℂ w.

theorem TauCeti.oddPeriodPolynomial_bijective {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : Function.Bijective ⇑(oddPeriodPolynomial hk)

The odd period-polynomial map is bijective.

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

The odd Eichler–Shimura isomorphism S_k(SL(2, ℤ)) ≃ₗ[ℂ] W_w^- (k = w + 2).

@[simp]

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

Applying oddPeriodPolynomialEquiv hk computes oddPeriodPolynomial hk.

@[simp]

theorem TauCeti.oddPeriodPolynomialEquiv_toLinearMap {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : ↑(oddPeriodPolynomialEquiv hk) = oddPeriodPolynomial hk

The underlying linear map of oddPeriodPolynomialEquiv hk is oddPeriodPolynomial hk.

Disjointness of X^w - Y^w and the even Eichler–Shimura isomorphism

theorem TauCeti.eisensteinPeriodPolynomial_notMem_range_evenPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (hw₀ : w ≠ 0) : ⟨eisensteinPeriodPolynomial ℂ w, ⋯⟩ ∉ (evenPeriodPolynomial hk).range

The Eisenstein period polynomial X^w - Y^w is not the even period polynomial of any cusp form in positive even degree w.

theorem TauCeti.isCompl_range_evenPeriodPolynomial_span_eisensteinPeriodPolynomial {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (hw₀ : w ≠ 0) : IsCompl (evenPeriodPolynomial hk).range (ℂ ∙ ⟨eisensteinPeriodPolynomial ℂ w, ⋯⟩)

In positive even degree w, W_w^+ is the internal direct sum of r^+(S_{w+2}) and ℂ · (X^w - Y^w) (Manin; Kohnen–Zagier, §1.1; Popa–Zagier, §2).

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

The extended even Eichler–Shimura isomorphism M_k(SL(2, ℤ)) ≃ₗ[ℂ] W_w^+ (k = w + 2), restricting to evenPeriodPolynomial hk on CuspForm 𝒮ℒ k and sending ModularForm.E to X^w - Y^w in positive even degree w (and identifying the zero spaces when w = 0 or w is odd).

@[simp]

theorem TauCeti.extendedEvenPeriodPolynomialEquiv_coe_cuspForm {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : (extendedEvenPeriodPolynomialEquiv hk) (ModularFormClass.modularForm g) = (evenPeriodPolynomial hk) g

On a cusp form g, extendedEvenPeriodPolynomialEquiv hk agrees with evenPeriodPolynomial hk in every degree w.

@[simp]

theorem TauCeti.extendedEvenPeriodPolynomialEquiv_E {k w : ℕ} (hk : ↑k = ↑w + 2) (hw : Even w) (hw₀ : w ≠ 0) (hk3 : 3 ≤ k) : (extendedEvenPeriodPolynomialEquiv hk) (ModularForm.E hk3) = ⟨eisensteinPeriodPolynomial ℂ w, ⋯⟩

In positive even degree w, extendedEvenPeriodPolynomialEquiv sends the normalized Eisenstein series ModularForm.E to the Eisenstein period polynomial X^w - Y^w.

The full Eichler–Shimura isomorphism onto periodPolynomials ℂ w

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

The full Eichler–Shimura period-polynomial isomorphism (M_k(SL(2, ℤ)) × S_k(SL(2, ℤ))) ≃ₗ[ℂ] W_w (k = w + 2), combining extendedEvenPeriodPolynomialEquiv hk and oddPeriodPolynomialEquiv hk.

@[simp]

theorem TauCeti.coe_periodPolynomialEquiv_apply {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (fg : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k × CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ↑((periodPolynomialEquiv hk) fg) = ↑((extendedEvenPeriodPolynomialEquiv hk) fg.1) + ↑((oddPeriodPolynomialEquiv hk) fg.2)

In homogeneousSubmodule (Fin 2) ℂ w, periodPolynomialEquiv hk (f, g) is the sum of the extended even period polynomial of f and the odd period polynomial of g.

@[simp]

theorem TauCeti.periodPolynomialEquiv_coe_cuspForm_same {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : (periodPolynomialEquiv hk) (ModularFormClass.modularForm g, g) = (periodPolynomial hk) g

On the diagonal (g, g) of a cusp form g, periodPolynomialEquiv hk recovers the full period polynomial r_g = r_g^+ + r_g^-.

Hecke equivariance and trace transfer to the Eichler–Selberg trace formula

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_extendedEvenPeriodPolynomialEquiv {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (F : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ((periodAction hw) ξ) ↑((extendedEvenPeriodPolynomialEquiv hk) F) = ↑((extendedEvenPeriodPolynomialEquiv hk) ((heckeTLevelOne k n) F))

Hecke equivariance of extendedEvenPeriodPolynomialEquiv. Every solution ξ of Popa–Zagier's period relation (A) intertwines heckeTLevelOne k n on ModularForm 𝒮ℒ k with periodAction hw ξ on evenPeriodPolynomials ℂ w.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_periodPolynomialEquiv {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (fg : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k × CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ((periodAction hw) ξ) ↑((periodPolynomialEquiv hk) fg) = ↑((periodPolynomialEquiv hk) ((heckeTLevelOne k n) fg.1, (heckeTCuspLevelOne k n) fg.2))

Hecke equivariance of periodPolynomialEquiv. Every solution ξ of Popa–Zagier's period relation (A) intertwines heckeTLevelOne k n × heckeTCuspLevelOne k n with periodAction hw ξ on periodPolynomials ℂ w.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_mem_periodPolynomials {w : ℕ} (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) ℂ w)} (hP : P ∈ periodPolynomials ℂ w) : ((periodAction hw) ξ) P ∈ periodPolynomials ℂ w

Every solution ξ of Popa–Zagier's period relation (A) preserves periodPolynomials ℂ w.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.trace_periodAction_restrict {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (hsub : ∀ P ∈ periodPolynomials ℂ w, ((periodAction hw) ξ) P ∈ periodPolynomials ℂ w := ⋯) : (LinearMap.trace ℂ ↥(periodPolynomials ℂ w)) (LinearMap.restrict ((periodAction hw) ξ) hsub) = (LinearMap.trace ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)) (heckeTLevelOne k n) + (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)) (heckeTCuspLevelOne k n)

Trace of a solution of the period relation (A) on periodPolynomials ℂ w. Across the Eichler–Shimura isomorphism periodPolynomialEquiv hk, the restriction of periodAction hw ξ to W_w is conjugate to heckeTLevelOne k n × heckeTCuspLevelOne k n, so its trace is Tr(Tₙ | M_k) + Tr(Tₙ | S_k).

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.trace_periodAction_eq {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (hw₀ : w ≠ 0) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (hP : PeriodRelation ℂ (↑n) ξ) (hX : ExchangeRelations ℂ (↑n) ξ) : (LinearMap.trace ℂ ↥(MvPolynomial.homogeneousSubmodule (Fin 2) ℂ w)) ((periodAction hw) ξ) = 2 * (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)) (heckeTCuspLevelOne k n) + ↑((ArithmeticFunction.sigma (w + 1)) n)

Popa–Zagier's ambient trace identity (Popa–Zagier, §2, Propositions 2 and 3): for positive even w, k = w + 2, n ≥ 1, and any ξ ∈ ℂ[ℳₙ] satisfying both the period relation (A) and the exchange relations (B), the trace of ξ on the ambient space V_w of degree-w binary forms is 2 Tr(Tₙ | S_k(SL(2, ℤ))) + σ_{w+1}(n).

theorem TauCeti.TraceFormulaMatrixModule.trace_heckeTCuspLevelOne_eq_trace_popaZagierElement {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) (hw : Even w) (hw₀ : w ≠ 0) (n : ℕ) [NeZero n] : (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)) (heckeTCuspLevelOne k n) = ((LinearMap.trace ℂ ↥(MvPolynomial.homogeneousSubmodule (Fin 2) ℂ w)) ((periodAction hw) (popaZagierElement ℂ ↑n)) - ↑((ArithmeticFunction.sigma (w + 1)) n)) / 2

Reduction of the level-one cusp-form Hecke trace to Popa–Zagier's explicit element: for positive even w, k = w + 2, and n ≥ 1, Tr(Tₙ | S_k(SL(2, ℤ))) = (Tr(popaZagierElement ℂ n | V_w) - σ_{w+1}(n)) / 2.