The dimension of the space of period polynomials

Let K be a field of characteristic zero and w a positive even integer. The period-polynomial space W_w = A ∩ B is cut out of the (w + 1)-dimensional space V_w of binary forms of degree w by A = ker (1 + S) and B = ker (1 + U + U²), where S and U = T S act with S² = 1 and U³ = 1. Its dimension is computed here by finite linear algebra, with no modular forms involved:

• the dimension of the kernel of 1 + S, respectively 1 + U + U², is read off the traces of S, respectively of U and U², on V_w (TauCeti.LinearMap.two_mul_finrank_ker_one_add_of_sq_eq_one and TauCeti.LinearMap.three_mul_finrank_ker_one_add_add_sq_of_pow_three_eq_one);
• these traces are the Eichler–Selberg weights P_{w+2}(t, 1) at the traces t = 0, 1, -1 of S, U and U², periodic in w (TauCeti.trace_binaryFormRep_eq_dickson_eval), which gives dim A = 2 ⌈w / 4⌉ and dim B = 2 ⌈w / 3⌉;
• A + B = V_w (TauCeti.codisjoint_ker_one_add_S_ker_one_add_U_add_U_sq), so dim W_w = dim A + dim B - (w + 1).

Comparing with Mathlib's level-one dimension formula ModularForm.dimension_level_one shows that dim W_w = dim M_{w+2}(SL(2, ℤ)) + dim S_{w+2}(SL(2, ℤ)) for every w. This is the dimension count by which the Eichler–Shimura period maps S_k → W_w⁻ and M_k → W_w⁺, once known to be injective, are isomorphisms: the even and odd parts W_w^± together span W_w (TauCeti.evenPeriodPolynomials_sup_oddPeriodPolynomials).

Main results

• TauCeti.finrank_ker_one_add_S: for even w, dim ker (1 + S) = 2 ⌈w / 4⌉ on V_w.
• TauCeti.finrank_ker_one_add_U_add_U_sq: for even w, dim ker (1 + U + U²) = 2 ⌈w / 3⌉ on V_w.
• TauCeti.finrank_periodPolynomials_add_eq: for positive even w, dim W_w + (w + 1) = 2 ⌈w / 4⌉ + 2 ⌈w / 3⌉.
• TauCeti.periodPolynomials_zero: W_0 = 0.
• TauCeti.finrank_periodPolynomials_eq_finrank_modularForm_add_finrank_cuspForm: for every w, dim W_w = dim M_{w+2}(SL(2, ℤ)) + dim S_{w+2}(SL(2, ℤ)) over ℂ.

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.

The traces of S, U and U² on binary forms

The dimensions of ker (1 + S) and ker (1 + U + U²)

theorem TauCeti.finrank_ker_one_add_S {K : Type u_1} [Field K] {w : ℕ} [CharZero K] (hw : Even w) : Module.finrank K ↥(1 + (binaryFormRep K w) (MulOpposite.op ↑ModularGroup.S)).ker = 2 * ((w + 3) / 4)

The binary forms of even degree w negated by S form a space of dimension 2 ⌈w / 4⌉.

theorem TauCeti.finrank_ker_one_add_U_add_U_sq {K : Type u_1} [Field K] {w : ℕ} [CharZero K] (hw : Even w) : Module.finrank K ↥(1 + (binaryFormRep K w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) + (binaryFormRep K w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) ^ 2).ker = 2 * ((w + 2) / 3)

The binary forms of even degree w killed by 1 + U + U² form a space of dimension 2 ⌈w / 3⌉.

The dimension of W_w

theorem TauCeti.finrank_periodPolynomials_add_eq {K : Type u_1} [Field K] {w : ℕ} [CharZero K] (hw : Even w) (hw₀ : w ≠ 0) : Module.finrank K ↥(periodPolynomials K w) + (w + 1) = 2 * ((w + 3) / 4) + 2 * ((w + 2) / 3)

The dimension of the period-polynomial space, computed by linear algebra: for positive even w, dim W_w = 2 ⌈w / 4⌉ + 2 ⌈w / 3⌉ - (w + 1), stated without truncated subtraction.

@[simp]

theorem TauCeti.periodPolynomials_zero {K : Type u_1} [Field K] : periodPolynomials K 0 = ⊥

In degree 0 there are no nonzero period polynomials, over every field: S and U fix the constants, so 1 + S = 2 and 1 + U + U² = 3 on V_0, and a vector killed by both is 0.

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

The period-polynomial space has the dimension of M_{w+2} ⊕ S_{w+2}: over ℂ, dim W_w = dim M_{w+2}(SL(2, ℤ)) + dim S_{w+2}(SL(2, ℤ)) for every w.

The left side is computed by linear algebra on binary forms (finrank_periodPolynomials_add_eq), the right side by Mathlib's level-one dimension formula. For w = 0 and for odd w both sides vanish. This is the dimension count which, together with the injectivity of the Eichler–Shimura period maps S_{w+2} → W_w⁻ and M_{w+2} → W_w⁺, makes them isomorphisms.