The space of period polynomials

Fix a commutative ring R and a natural number w (the weight k = w + 2). Let V_w be the R-module of binary forms of degree w, modelled as homogeneousSubmodule (Fin 2) R w with X = X 0 and Y = X 1. Integral 2 × 2 matrices act on it on the right, (P ∣ M)(X, Y) = P(aX + bY, cX + dY) for M = !![a, b; c, d], so that P ∣ (M * N) = (P ∣ M) ∣ N; this is TauCeti.binaryFormRep, defined in TauCeti.NumberTheory.ModularForms.BinaryForms. The period-polynomial space is W_w = ker(1 + S) ∩ ker(1 + U + U²), where S = !![0, -1; 1, 0] and U = T S = !![1, -1; 1, 0] are the standard generators of order 2 and 3 of PSL(2, ℤ). It is the space in which the period polynomial r_f(X, Y) = ∫₀^{i∞} f(τ) (X - τY)^w dτ of a cusp form f of weight w + 2 lives, and the target of the Eichler–Shimura period maps. Popa and Zagier compute the trace of Hecke operators on S_k(SL(2, ℤ)) by computing it on W_w.

The parity involution is ε = !![-1, 0; 0, 1], acting by P(X, Y) ↦ P(-X, Y). For even w it preserves W_w (because εSε = -S and εUε = SU²S), and the even and odd period polynomials W_w^± are its ±1-eigenspaces in W_w. When 2 is invertible they span W_w. For odd w the central element S² = -1 acts by -1, so W_w = 0 whenever multiplication by 2 is injective on R; under this condition only even w, that is even weight, carries period polynomials.

The Eisenstein polynomial X^w - Y^w is an even period polynomial for every even w. For positive even w, over ℂ, it is up to a nonzero scalar the extended even period polynomial of the Eisenstein series of weight w + 2; at w = 0 it is zero.

Over a field of characteristic zero and for positive even w, the two kernels A = ker(1 + S) and B = ker(1 + U + U²) cutting out W_w together span V_w. Popa and Zagier use this to reduce the trace of an operator exchanging A and B on W_w to its trace on V_w.

Main definitions

• TauCeti.periodPolynomials R w: the period-polynomial space W_w.
• TauCeti.evenPeriodPolynomials R w, TauCeti.oddPeriodPolynomials R w: its even and odd parts W_w^±.
• TauCeti.eisensteinPeriodPolynomial R w: the binary form X^w - Y^w.

Main results

• TauCeti.binaryFormRep_parity_involutive: the parity action is an involution.
• TauCeti.mem_periodPolynomials_binaryFormRep_parity: for even w, the parity involution preserves W_w.
• TauCeti.evenPeriodPolynomials_sup_oddPeriodPolynomials, TauCeti.disjoint_evenPeriodPolynomials_oddPeriodPolynomials, and TauCeti.isCompl_evenPeriodPolynomials_oddPeriodPolynomials: W_w = W_w^+ ⊕ W_w^- when 2 is invertible (spanning and complementarity) and multiplication by 2 is injective (disjointness).
• TauCeti.periodPolynomials_eq_bot_of_odd: W_w = 0 for odd w when multiplication by 2 is injective.
• TauCeti.mem_evenPeriodPolynomials_eisensteinPeriodPolynomial: X^w - Y^w ∈ W_w^+ for even w.
• TauCeti.evenPeriodPolynomials_ne_bot, TauCeti.periodPolynomials_ne_bot: W_w^+ and W_w are nonzero for positive even w over a nontrivial ring, witnessed by X^w - Y^w.
• TauCeti.binaryFormRep_S_sq_of_even, TauCeti.binaryFormRep_U_pow_three_of_even: for even w, S and U act on V_w with orders dividing 2 and 3, since -1 acts trivially.
• TauCeti.codisjoint_ker_one_add_S_ker_one_add_U_add_U_sq: over a field of characteristic zero, ker(1 + S) + ker(1 + U + U²) = V_w for positive even w.

Implementation notes

Popa and Zagier prove ker(1 + S) + ker(1 + U + U²) = V_w with a nondegenerate SL(2, ℤ)-invariant pairing on V_w. Here it is proved directly. For even w, S² = 1 and U³ = 1 on V_w, so P - P ∣ S lies in ker(1 + S) and P - P ∣ U lies in ker(1 + U + U²) (TauCeti.End.range_one_sub_le_ker_one_add, TauCeti.End.range_one_sub_le_ker_one_add_add_sq), and P - P ∣ T lies in their sum, as T = -U S. The substitution T : X ↦ X + Y is unitriangular on the monomials X^a Y^b, so induction on a puts every X^a Y^b with a < w in the sum, and then X^w = Y^w - (Y^w - Y^w ∣ S) as well.

References

• 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.
• W. Kohnen and D. Zagier, Modular forms with rational periods, in Modular Forms (R. A. Rankin, ed.), Ellis Horwood, 1984, 197–249, §1.

noncomputable def TauCeti.periodPolynomials (R : Type u_1) [CommRing R] (w : ℕ) : Submodule R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The period-polynomial space W_w = ker(1 + S) ∩ ker(1 + U + U²) inside the binary forms of degree w, where S = !![0, -1; 1, 0] and U = T S = !![1, -1; 1, 0].

theorem TauCeti.periodPolynomials_def {R : Type u_1} [CommRing R] {w : ℕ} : periodPolynomials R w = (1 + (binaryFormRep R w) (MulOpposite.op ↑ModularGroup.S)).ker ⊓ (1 + (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) + (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) ^ 2).ker

Definition of the period-polynomial space.

@[simp]

theorem TauCeti.mem_periodPolynomials_iff {R : Type u_1} [CommRing R] {w : ℕ} {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} : P ∈ periodPolynomials R w ↔ P + ((binaryFormRep R w) (MulOpposite.op ↑ModularGroup.S)) P = 0 ∧ P + ((binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S))) P + ((binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S))) (((binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S))) P) = 0

A binary form P of degree w is a period polynomial iff P + P ∣ S = 0 and P + P ∣ U + P ∣ U² = 0.

noncomputable def TauCeti.evenPeriodPolynomials (R : Type u_1) [CommRing R] (w : ℕ) : Submodule R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The even period polynomials W_w^+: the period polynomials fixed by the parity involution P(X, Y) ↦ P(-X, Y).

theorem TauCeti.evenPeriodPolynomials_def (R : Type u_1) [CommRing R] (w : ℕ) : evenPeriodPolynomials R w = periodPolynomials R w ⊓ ((binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1]) - 1).ker

Definition of the even period-polynomial space.

noncomputable def TauCeti.oddPeriodPolynomials (R : Type u_1) [CommRing R] (w : ℕ) : Submodule R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The odd period polynomials W_w^-: the period polynomials negated by the parity involution P(X, Y) ↦ P(-X, Y).

theorem TauCeti.oddPeriodPolynomials_def (R : Type u_1) [CommRing R] (w : ℕ) : oddPeriodPolynomials R w = periodPolynomials R w ⊓ ((binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1]) + 1).ker

Definition of the odd period-polynomial space.

@[simp]

theorem TauCeti.mem_evenPeriodPolynomials_iff {R : Type u_1} [CommRing R] {w : ℕ} {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} : P ∈ evenPeriodPolynomials R w ↔ P ∈ periodPolynomials R w ∧ ((binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1])) P = P

@[simp]

theorem TauCeti.mem_oddPeriodPolynomials_iff {R : Type u_1} [CommRing R] {w : ℕ} {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} : P ∈ oddPeriodPolynomials R w ↔ P ∈ periodPolynomials R w ∧ ((binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1])) P = -P

The parity involution preserves the period polynomials

theorem TauCeti.parity_mul_S : !![-1, 0; 0, 1] * ↑ModularGroup.S = -(↑ModularGroup.S * !![-1, 0; 0, 1])

εSε = -S, in the form ε S = -(S ε).

theorem TauCeti.parity_mul_T_zpow (m : ℤ) : !![-1, 0; 0, 1] * ↑(ModularGroup.T ^ m) = ↑(ModularGroup.T ^ (-m)) * !![-1, 0; 0, 1]

εTᵐε = T⁻ᵐ, in the form ε Tᵐ = T⁻ᵐ ε.

theorem TauCeti.parity_mul_parity : !![-1, 0; 0, 1] * !![-1, 0; 0, 1] = 1

The parity involution squares to the identity.

theorem TauCeti.binaryFormRep_parity_involutive {R : Type u_1} [CommRing R] {w : ℕ} : Function.Involutive ⇑((binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1]))

The parity action P(X, Y) ↦ P(-X, Y) is an involution.

theorem TauCeti.mem_periodPolynomials_binaryFormRep_parity {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} (hP : P ∈ periodPolynomials R w) : ((binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1])) P ∈ periodPolynomials R w

For even w, the parity involution P(X, Y) ↦ P(-X, Y) preserves the period polynomials.

The even and odd parts

theorem TauCeti.disjoint_evenPeriodPolynomials_oddPeriodPolynomials {R : Type u_1} [CommRing R] {w : ℕ} (h2 : Function.Injective fun (r : R) => 2 * r) : Disjoint (evenPeriodPolynomials R w) (oddPeriodPolynomials R w)

A period polynomial cannot be both even and odd when multiplication by 2 is injective.

theorem TauCeti.periodPolynomials_eq_bot_of_odd {R : Type u_1} [CommRing R] {w : ℕ} (h2 : Function.Injective fun (r : R) => 2 * r) (hw : Odd w) : periodPolynomials R w = ⊥

For odd w there are no nonzero period polynomials when multiplication by 2 is injective: the central element S² = -1 acts by -1 but fixes every P with P ∣ S = -P.

theorem TauCeti.evenPeriodPolynomials_sup_oddPeriodPolynomials {R : Type u_1} [CommRing R] {w : ℕ} [Invertible 2] : evenPeriodPolynomials R w ⊔ oddPeriodPolynomials R w = periodPolynomials R w

When 2 is invertible, the even and odd period polynomials span W_w.

theorem TauCeti.isCompl_evenPeriodPolynomials_oddPeriodPolynomials {R : Type u_1} [CommRing R] [Invertible 2] (w : ℕ) : IsCompl (Submodule.comap (periodPolynomials R w).subtype (evenPeriodPolynomials R w)) (Submodule.comap (periodPolynomials R w).subtype (oddPeriodPolynomials R w))

When 2 is invertible, W_w is the internal direct sum of W_w^+ and W_w^-.

The Eisenstein polynomial

noncomputable def TauCeti.eisensteinPeriodPolynomial (R : Type u_1) [CommRing R] (w : ℕ) : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The binary form X^w - Y^w. For even w it is an even period polynomial. For positive even w, over ℂ, it is up to a nonzero scalar the extended even period polynomial of the Eisenstein series of weight w + 2; at w = 0 it is zero.

@[simp]

theorem TauCeti.coe_eisensteinPeriodPolynomial {R : Type u_1} [CommRing R] {w : ℕ} : ↑(eisensteinPeriodPolynomial R w) = MvPolynomial.X 0 ^ w - MvPolynomial.X 1 ^ w

theorem TauCeti.mem_evenPeriodPolynomials_eisensteinPeriodPolynomial {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) : eisensteinPeriodPolynomial R w ∈ evenPeriodPolynomials R w

For even w, the Eisenstein polynomial X^w - Y^w is an even period polynomial.

theorem TauCeti.eisensteinPeriodPolynomial_ne_zero {R : Type u_1} [CommRing R] {w : ℕ} [Nontrivial R] (hw : w ≠ 0) : eisensteinPeriodPolynomial R w ≠ 0

For positive w, the Eisenstein polynomial X^w - Y^w is nonzero.

theorem TauCeti.evenPeriodPolynomials_ne_bot {R : Type u_1} [CommRing R] {w : ℕ} [Nontrivial R] (hw : Even w) (hw₀ : w ≠ 0) : evenPeriodPolynomials R w ≠ ⊥

For positive even w over a nontrivial ring, the even period polynomials are nonzero.

theorem TauCeti.periodPolynomials_ne_bot {R : Type u_1} [CommRing R] {w : ℕ} [Nontrivial R] (hw : Even w) (hw₀ : w ≠ 0) : periodPolynomials R w ≠ ⊥

For positive even w over a nontrivial ring, the period polynomials are nonzero.

The kernels of 1 + S and 1 + U + U² span V_w

theorem TauCeti.binaryFormRep_S_sq_of_even {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) : (binaryFormRep R w) (MulOpposite.op ↑ModularGroup.S) ^ 2 = 1

For even w, S acts on V_w as an involution, since S² = -1 acts trivially.

theorem TauCeti.binaryFormRep_U_pow_three_of_even {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) : (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) ^ 3 = 1

For even w, U = T S acts on V_w with cube 1, since U³ = -1 acts trivially.

theorem TauCeti.codisjoint_ker_one_add_S_ker_one_add_U_add_U_sq {w : ℕ} {K : Type u_2} [Field K] [CharZero K] (hw : Even w) (hw₀ : w ≠ 0) : Codisjoint (1 + (binaryFormRep K w) (MulOpposite.op ↑ModularGroup.S)).ker (1 + (binaryFormRep K w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) + (binaryFormRep K w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) ^ 2).ker

The kernels of 1 + S and 1 + U + U² span V_w (Popa–Zagier, §2, proof of Proposition 3): over a field of characteristic zero and for even w ≠ 0, every binary form of degree w is the sum of one killed by 1 + S and one killed by 1 + U + U², where U = T S. Both hypotheses on w are needed: for w = 0 or odd w both kernels are zero.