The Popa–Zagier period relation

Popa and Zagier's proof of the Eichler–Selberg trace formula starts from an element ξ of the group ring ℛₙ = ℚ[ℳₙ] (written Tₙ with a tilde in their paper) satisfying the period relation (A) (1 - S)·ξ - Tₙ^∞·(1 - S) ∈ (1 - T)·ℛₙ, where S = (0 -1; 1 0) and T = (1 1; 0 1) act on ℳₙ by left and right multiplication and Tₙ^∞ is the formal sum of the upper-triangular representatives of Γ \ ℳₙ. This file defines the predicate TauCeti.TraceFormulaMatrixModule.PeriodRelation k n ξ expressing (A) for ξ ∈ ℛₙ and proves that it has a solution for every n.

By Popa–Zagier's Proposition 2, every solution of (A) acts on period polynomials as the Hecke operator Tₙ. Solutions exist for every n; as in Popa–Zagier, who say that they exist "as in [CZ]", this is an existence statement, without an explicit solution. Two solutions differ by an element η with (1 - S)·η ∈ (1 - T)·ℛₙ. Popa and Zagier also give an explicit solution, their eq. (15), and deduce (A) for it from the exchange relations (B) and the coset identity ⟨ξ, K⟩ = -1. That deduction is TauCeti.TraceFormulaMatrixModule.periodRelation_popaZagierElement.

Membership in (1 - T)·ℛₙ is decided by the criterion of Popa–Zagier §3: an element of ℛₙ lies in (1 - T)·ℛₙ if and only if its coefficients sum to zero along every orbit of Γ_∞ = ⟨T⟩ on ℳₙ.

Main definitions

• TauCeti.TraceFormulaMatrixModule.PeriodRelation k n ξ: the element ξ ∈ ℛₙ satisfies the period relation (A).

Main results

• TauCeti.TraceFormulaMatrixModule.mem_range_one_sub_T_iff: an element of k[ℳₙ] lies in (1 - T)·k[ℳₙ] if and only if its coefficient sums along the ⟨T⟩-orbits vanish.
• TauCeti.TraceFormulaMatrixModule.one_sub_ofMulAction_T_injective: for n ≠ 0, left multiplication by 1 - T is injective on k[ℳₙ].
• TauCeti.TraceFormulaMatrixModule.PeriodRelation.add and TauCeti.TraceFormulaMatrixModule.PeriodRelation.sub_mem: solutions of (A) are determined up to elements η with (1 - S)·η ∈ (1 - T)·ℛₙ.
• TauCeti.TraceFormulaMatrixModule.exists_periodRelation: the period relation (A) has a solution for every n.

Implementation notes

The products in (A) are permutation representations on ℛₙ. The left products are the representation of SL(2, ℤ): S·ξ is Representation.ofMulAction ℚ SL(2, ℤ) ℳₙ S ξ, and similarly for T. This is the simp-normal form of the left representation of PSL(2, ℤ) at the classes of S and T (by TauCeti.TraceFormulaMatrixModule.ofMulAction_coe). The right product ξ·S is Representation.ofMulAction ℚ PSL(2, ℤ)ᵐᵒᵖ ℳₙ (MulOpposite.op S) ξ, the right representation of PSL(2, ℤ) from TauCeti.NumberTheory.ModularForms.LevelOne.TraceFormula.PermutationModule, with S viewed in PSL(2, ℤ). The matrices S and T are Mathlib's ModularGroup.S and ModularGroup.T; they are Popa–Zagier's S and T.

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. The period relation (A) is stated in §1; the criterion for membership in (1 - T)·ℛₙ is in §3, which also notes that solutions of (A) exist "as in [CZ]".
• [CZ] Y. J. Choie and D. Zagier, Rational period functions for PSL(2, ℤ), Contemp. Math. 143 (1993), 89–108.

def TauCeti.TraceFormulaMatrixModule.PeriodRelation (k : Type u_1) [CommRing k] (n : ℤ) (ξ : MonoidAlgebra k (TraceFormulaMatrixModule n)) : Prop

Popa–Zagier's period relation (A) for ξ ∈ k[ℳₙ] (Popa–Zagier take k = ℚ, ℛₙ = ℚ[ℳₙ]): (1 - S)·ξ - Tₙ^∞·(1 - S) ∈ (1 - T)·ℛₙ, where (1 - S)· and (1 - T)· are left multiplications and ·(1 - S) is right multiplication.

theorem TauCeti.TraceFormulaMatrixModule.periodRelation_iff {k : Type u_1} [CommRing k] {n : ℤ} {ξ : MonoidAlgebra k (TraceFormulaMatrixModule n)} : PeriodRelation k n ξ ↔ (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.S) ξ - (1 - (Representation.ofMulAction k (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)) (MulOpposite.op ↑ModularGroup.S)) (upperTriangularSum k n) ∈ (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.T).range

Unfolding PeriodRelation.

theorem TauCeti.TraceFormulaMatrixModule.mem_range_one_sub_T_iff {k : Type u_1} [CommRing k] {n : ℤ} {ζ : MonoidAlgebra k (TraceFormulaMatrixModule n)} : ζ ∈ (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.T).range ↔ (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel (↥(Subgroup.zpowers ModularGroup.T)) (TraceFormulaMatrixModule n)))) ζ = 0

Popa–Zagier's criterion for (1 - T)·ℛₙ. An element of k[ℳₙ] lies in the range of left multiplication by 1 - T if and only if its coefficients sum to zero along every orbit of Γ_∞ = ⟨T⟩.

theorem TauCeti.TraceFormulaMatrixModule.one_sub_ofMulAction_T_injective {k : Type u_1} [CommRing k] {n : ℤ} (hn : n ≠ 0) : Function.Injective ⇑(1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.T)

For n ≠ 0, left multiplication by 1 - T is injective on k[ℳₙ]: the orbits of ⟨T⟩ on ℳₙ are infinite, and elements of k[ℳₙ] are finitely supported. In particular the witness of the period relation (A) is unique.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.add {k : Type u_1} [CommRing k] {n : ℤ} {ξ η : MonoidAlgebra k (TraceFormulaMatrixModule n)} (h : PeriodRelation k n ξ) (hη : (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.S) η ∈ (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.T).range) : PeriodRelation k n (ξ + η)

Adding to a solution of the period relation an element η with (1 - S)·η ∈ (1 - T)·ℛₙ gives another solution.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.sub_mem {k : Type u_1} [CommRing k] {n : ℤ} {ξ ξ' : MonoidAlgebra k (TraceFormulaMatrixModule n)} (h : PeriodRelation k n ξ) (h' : PeriodRelation k n ξ') : (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.S) (ξ - ξ') ∈ (1 - (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.T).range

Two solutions of the period relation differ by an element η with (1 - S)·η ∈ (1 - T)·ℛₙ.

theorem TauCeti.TraceFormulaMatrixModule.exists_periodRelation (k : Type u_1) [CommRing k] (n : ℤ) : ∃ (ξ : MonoidAlgebra k (TraceFormulaMatrixModule n)), PeriodRelation k n ξ

Existence of a solution of the period relation (A) (Popa–Zagier, "as in [CZ]"): for every n there is ξ ∈ ℛₙ with (1 - S)·ξ - Tₙ^∞·(1 - S) ∈ (1 - T)·ℛₙ.