The parity symmetry of the period relation and Hecke equivariance of r_f^±

Let ε = !![-1, 0; 0, 1]. Conjugation A ↦ ε A ε sends a determinant-n matrix (a b; c d) to (a -b; -c d), again of determinant n, and descends to an involution of the projective matrix module ℳₙ. It normalizes the data of Popa and Zagier's period relation

(A) (1 - S)·ξ - Tₙ^∞·(1 - S) ∈ (1 - T)·ℛₙ:

ε S ε = -S acts on ℳₙ as S, on the left and on the right; ε T ε = T⁻¹, so the ideal (1 - T)·ℛₙ is preserved; and each upper-triangular representative (a b; 0 d) of Γ \ ℳₙ goes to (a -b; 0 d), which lies in the ⟨T⟩-orbit of another representative, so the conjugate of Tₙ^∞ has the same ⟨T⟩-orbit sums as Tₙ^∞. Hence the conjugate of a solution of (A) is again a solution.

The conjugate of ξ acts on binary forms by P ↦ ((P ∣ ε) ∣ ξ) ∣ ε. Every solution of (A) acts on the period polynomials of level-one cusp forms as the Hecke operator Tₙ (Popa–Zagier, Proposition 2). Applying this to ξ and to its conjugate shows that the action of ξ commutes with the parity involution P(X, Y) ↦ P(-X, Y) on period polynomials of cusp forms: (r_f ∣ ε) ∣ ξ = r_{Tₙ f} ∣ ε. Consequently the even and odd period polynomials are Hecke-equivariant, r_f^± ∣ ξ = r_{Tₙ f}^±: the maps f ↦ r_f^± from S_k(SL(2, ℤ)) to W_w^± intertwine Tₙ with the action of any solution of (A), such as Popa and Zagier's explicit element.

Main definitions

• TauCeti.TraceFormulaMatrix.parityConj: the conjugate ε A ε of a determinant-n matrix.
• TauCeti.TraceFormulaMatrixModule.parityConj: the induced involution of ℳₙ.

Main results

• TauCeti.TraceFormulaMatrixModule.mapDomainLinearMap_parityConj_upperTriangularSum_sub_mem: the conjugate of Tₙ^∞ is congruent to Tₙ^∞ modulo (1 - T)·ℛₙ.
• TauCeti.TraceFormulaMatrixModule.PeriodRelation.mapDomainLinearMap_parityConj: the conjugate of a solution of the period relation (A) is a solution.
• TauCeti.TraceFormulaMatrixModule.periodAction_mapDomainLinearMap_parityConj: the conjugate of ξ acts on binary forms by P ↦ ((P ∣ ε) ∣ ξ) ∣ ε.
• TraceFormulaMatrixModule.PeriodRelation.periodAction_binaryFormRep_parity_periodPolynomial: (r_f ∣ ε) ∣ ξ = r_{Tₙ f} ∣ ε for every solution ξ of (A).
• TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_evenPeriodPolynomial and TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_oddPeriodPolynomial: r_f^± ∣ ξ = r_{Tₙ f}^±.

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, §§1–2. The period relation (A) is stated in §1 and Proposition 2 is in §2.

def TauCeti.TraceFormulaMatrix.parityConj {n : ℤ} (A : TraceFormulaMatrix n) : TraceFormulaMatrix n

The conjugate ε A ε of a determinant-n matrix A = (a b; c d) by the parity matrix ε = !![-1, 0; 0, 1]: the matrix (a -b; -c d), again of determinant n.

@[simp]

theorem TauCeti.TraceFormulaMatrix.val_parityConj {n : ℤ} (A : TraceFormulaMatrix n) : ↑A.parityConj = !![-1, 0; 0, 1] * ↑A * !![-1, 0; 0, 1]

The underlying matrix of TraceFormulaMatrix.parityConj A is ε A ε.

@[simp]

theorem TauCeti.TraceFormulaMatrix.parityConj_neg {n : ℤ} (A : TraceFormulaMatrix n) : (-A).parityConj = -A.parityConj

Conjugation by the parity matrix commutes with negation.

def TauCeti.TraceFormulaMatrixModule.parityConj {n : ℤ} (x : TraceFormulaMatrixModule n) : TraceFormulaMatrixModule n

The involution of the projective matrix module ℳₙ induced by conjugation A ↦ ε A ε by the parity matrix ε = !![-1, 0; 0, 1].

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.parityConj_mk {n : ℤ} (A : TraceFormulaMatrix n) : (mk A).parityConj = mk A.parityConj

On a representative, the involution of ℳₙ is conjugation by the parity matrix.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.parityConj_parityConj {n : ℤ} (x : TraceFormulaMatrixModule n) : x.parityConj.parityConj = x

Conjugation by the parity matrix is an involution of ℳₙ.

theorem TauCeti.TraceFormulaMatrixModule.parityConj_involutive {n : ℤ} : Function.Involutive parityConj

Conjugation by the parity matrix is an involution of ℳₙ.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.parityConj_S_smul {n : ℤ} (x : TraceFormulaMatrixModule n) : (ModularGroup.S • x).parityConj = ModularGroup.S • x.parityConj

ε S ε = -S, so conjugation by the parity matrix commutes with left multiplication by S.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.parityConj_T_zpow_smul {n : ℤ} (m : ℤ) (x : TraceFormulaMatrixModule n) : (ModularGroup.T ^ m • x).parityConj = ModularGroup.T ^ (-m) • x.parityConj

ε T^m ε = T^(-m), so conjugation by the parity matrix turns left multiplication by T ^ m into left multiplication by T ^ (-m).

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.parityConj_T_smul {n : ℤ} (x : TraceFormulaMatrixModule n) : (ModularGroup.T • x).parityConj = ModularGroup.T⁻¹ • x.parityConj

ε T ε = T⁻¹, so conjugation by the parity matrix turns left multiplication by T into left multiplication by T⁻¹.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.parityConj_op_S_smul {n : ℤ} (x : TraceFormulaMatrixModule n) : (MulOpposite.op ↑ModularGroup.S • x).parityConj = MulOpposite.op ↑ModularGroup.S • x.parityConj

ε S ε = -S, so conjugation by the parity matrix commutes with right multiplication by S.

The conjugate of Tₙ^∞

theorem TauCeti.TraceFormulaMatrixModule.mapDomainLinearMap_parityConj_upperTriangularSum_sub_mem {n : ℤ} {R : Type u_1} [CommRing R] : (MonoidAlgebra.mapDomainLinearMap R R parityConj) (upperTriangularSum R n) - upperTriangularSum R n ∈ (1 - (Representation.ofMulAction R (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) ModularGroup.T).range

The conjugate of Tₙ^∞ by the parity matrix is Tₙ^∞ modulo (1 - T)·ℛₙ. Conjugation sends the representative (a b; 0 d) of ℳₙ^∞ to (a -b; 0 d), which lies in the ⟨T⟩-orbit of the representative (a b'; 0 d) with b' ≡ -b mod d.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.mapDomainLinearMap_parityConj {n : ℤ} {R : Type u_1} [CommRing R] {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (h : PeriodRelation R n ξ) : PeriodRelation R n ((MonoidAlgebra.mapDomainLinearMap R R parityConj) ξ)

The parity conjugate of a solution of the period relation is a solution. If ξ satisfies Popa–Zagier's period relation (A), then so does its image under conjugation M ↦ ε M ε by ε = !![-1, 0; 0, 1].

The action on binary forms

theorem TauCeti.TraceFormulaMatrixModule.periodAction_mapDomainLinearMap_parityConj {n : ℤ} {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) (ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)) : (periodAction hw) ((MonoidAlgebra.mapDomainLinearMap R R parityConj) ξ) = (binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1]) * (periodAction hw) ξ * (binaryFormRep R w) (MulOpposite.op !![-1, 0; 0, 1])

The parity conjugate acts by conjugating with the parity involution. The image of ξ under M ↦ ε M ε acts on binary forms of even degree by P ↦ ((P ∣ ε) ∣ ξ) ∣ ε.

Hecke equivariance of the even and odd period polynomials

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_binaryFormRep_parity_periodPolynomial {w : ℕ} {k : ℤ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ((periodAction hw) ξ) (((binaryFormRep ℂ w) (MulOpposite.op !![-1, 0; 0, 1])) ↑((periodPolynomial hk) f)) = ((binaryFormRep ℂ w) (MulOpposite.op !![-1, 0; 0, 1])) ↑((periodPolynomial hk) ((heckeTCuspLevelOne k n) f))

The Hecke action commutes with the parity involution on period polynomials. Let n ≥ 1 and let ξ be a solution of the period relation (A). For every level-one cusp form f of weight w + 2, (r_f ∣ ε) ∣ ξ = r_{Tₙ f} ∣ ε, where ε = !![-1, 0; 0, 1] acts by P(X, Y) ↦ P(-X, Y) and Tₙ = TauCeti.heckeTCuspLevelOne (w + 2) n.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_evenPeriodPolynomial {w : ℕ} {k : ℤ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ((periodAction hw) ξ) ↑((evenPeriodPolynomial hk) f) = ↑((evenPeriodPolynomial hk) ((heckeTCuspLevelOne k n) f))

Hecke equivariance of the even period polynomial. Let n ≥ 1 and let ξ be a solution of the period relation (A). For every level-one cusp form f of weight w + 2, r_f^+ ∣ ξ = r_{Tₙ f}^+, with Tₙ = TauCeti.heckeTCuspLevelOne (w + 2) n.

theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_oddPeriodPolynomial {w : ℕ} {k : ℤ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ((periodAction hw) ξ) ↑((oddPeriodPolynomial hk) f) = ↑((oddPeriodPolynomial hk) ((heckeTCuspLevelOne k n) f))

Hecke equivariance of the odd period polynomial. Let n ≥ 1 and let ξ be a solution of the period relation (A). For every level-one cusp form f of weight w + 2, r_f^- ∣ ξ = r_{Tₙ f}^-, with Tₙ = TauCeti.heckeTCuspLevelOne (w + 2) n.