The dimensions of the even and odd period-polynomial spaces

For positive even w, the even part of W_w has dimension one greater than the odd part. Together with the total dimension, this identifies their dimensions with those of modular forms and cusp forms of weight w + 2. These are the separate dimension counts needed to turn the even and odd period maps into the Eichler–Shimura isomorphisms.

The calculation is algebraic. The swap J : P(X,Y) ↦ P(Y,X) preserves both A = ker(1 + S) and B = ker(1 + U + U²). Its traces on A and B vanish, while its ambient trace is one. Inclusion-exclusion gives trace -1 on W_w = A ∩ B. On W_w, the swap is the negative of the parity involution, so the parity trace is one.

Main results

• finrank_evenPeriodPolynomials_eq_finrank_oddPeriodPolynomials_add_one: the algebraic dimension difference over a characteristic-zero field, in positive even degree.
• finrank_evenPeriodPolynomials_eq_finrank_modularForm and finrank_oddPeriodPolynomials_eq_finrank_cuspForm: the individual dimension comparisons over ℂ, in every degree.

References

• W. Kohnen and D. Zagier, Modular forms with rational periods, §1.
• A. Popa and D. Zagier, An elementary proof of the Eichler–Selberg trace formula, J. Reine Angew. Math. 762 (2020), 105–122, §2.

theorem TauCeti.finrank_evenPeriodPolynomials_eq_finrank_oddPeriodPolynomials_add_one {K : Type u_1} [Field K] {w : ℕ} [CharZero K] (hw : Even w) (hw₀ : w ≠ 0) : Module.finrank K ↥(evenPeriodPolynomials K w) = Module.finrank K ↥(oddPeriodPolynomials K w) + 1

In positive even degree, the even period-polynomial space has dimension one greater than the odd space, over any characteristic-zero field.

theorem TauCeti.finrank_evenPeriodPolynomials_eq_finrank_modularForm (w : ℕ) : Module.finrank ℂ ↥(evenPeriodPolynomials ℂ w) = Module.finrank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑(w + 2))

The even period polynomials of degree w have the dimension of the level-one modular forms of weight w + 2, including degree zero and odd degrees.

theorem TauCeti.finrank_oddPeriodPolynomials_eq_finrank_cuspForm (w : ℕ) : Module.finrank ℂ ↥(oddPeriodPolynomials ℂ w) = Module.finrank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑(w + 2))

The odd period polynomials of degree w have the dimension of the level-one cusp forms of weight w + 2, including degree zero and odd degrees.