The determinant-matrix action on period polynomials

For even w, the right substitution action of a determinant-n matrix on homogeneous binary forms of degree w depends only on its class modulo sign. Extending this action linearly gives an action of the matrix module used in the level-one trace formula. Popa and Zagier's exchange relations ensure that this action maps each of ker (1 + S) and ker (1 + U + U²), with U = T S, into the other, and hence preserves their intersection, the period-polynomial space.

Evaluating Popa and Zagier's period relation (A) on the monomial Y^w — which is fixed by T and sent to Y^w - X^w = -(X^w - Y^w) by 1 - S — also shows that every solution ξ of PeriodRelation R n ξ (n ≥ 1) scales the Eisenstein period polynomial X^w - Y^w by σ_{w+1}(n) (PeriodRelation.periodAction_eisensteinPeriodPolynomial).

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.

noncomputable def TauCeti.TraceFormulaMatrixModule.binaryFormAction {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (x : TraceFormulaMatrixModule n) : Module.End R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

Substitution by a projective determinant-n matrix on binary forms of even degree.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.binaryFormAction_mk {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (A : TraceFormulaMatrix n) : binaryFormAction hw (mk A) = (binaryFormRep R w) (MulOpposite.op ↑A)

On a representative, the projective action is the usual binary-form substitution.

noncomputable def TauCeti.TraceFormulaMatrixModule.periodAction {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) : MonoidAlgebra R (TraceFormulaMatrixModule n) →ₗ[R] Module.End R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

Linear extension of the determinant-matrix substitution to the free matrix module.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.periodAction_single {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (x : TraceFormulaMatrixModule n) (c : R) : (periodAction hw) (MonoidAlgebra.single x c) = c • binaryFormAction hw x

A basis element acts by its coefficient times the matrix substitution.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.binaryFormAction_smul {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : binaryFormAction hw (g • x) = binaryFormAction hw x * (binaryFormRep R w) (MulOpposite.op ↑g)

Left multiplication of a determinant matrix precomposes its substitution action.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.binaryFormAction_op_smul {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (x : TraceFormulaMatrixModule n) : binaryFormAction hw (MulOpposite.op ↑g • x) = (binaryFormRep R w) (MulOpposite.op ↑g) * binaryFormAction hw x

Right multiplication of a determinant matrix postcomposes its substitution action.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.periodAction_ofMulAction {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)) : (periodAction hw) (((Representation.ofMulAction R (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) g) ξ) = (periodAction hw) ξ * (binaryFormRep R w) (MulOpposite.op ↑g)

The free matrix action turns left multiplication in the matrix module into precomposition of substitutions.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.periodAction_ofMulAction_op {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)) : (periodAction hw) (((Representation.ofMulAction R (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)) (MulOpposite.op ↑g)) ξ) = (binaryFormRep R w) (MulOpposite.op ↑g) * (periodAction hw) ξ

The free matrix action turns right multiplication in the matrix module into postcomposition of substitutions.

theorem TauCeti.TraceFormulaMatrixModule.ExchangeRelations.periodAction_mem_ker_one_add_S {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (hξ : ExchangeRelations R n ξ) {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} (hP : P ∈ (1 + (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) + (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) ^ 2).ker) : ((periodAction hw) ξ) P ∈ (1 + (binaryFormRep R w) (MulOpposite.op ↑ModularGroup.S)).ker

The first exchange map. By the exchange relation ξ (1 + S) ∈ (1 + U + U²) ℛₙ, the action of ξ maps ker (1 + U + U²) into ker (1 + S), where U = T S.

theorem TauCeti.TraceFormulaMatrixModule.ExchangeRelations.periodAction_mem_ker_one_add_U_add_U_sq {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (hξ : ExchangeRelations R n ξ) {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} (hP : P ∈ (1 + (binaryFormRep R w) (MulOpposite.op ↑ModularGroup.S)).ker) : ((periodAction hw) ξ) P ∈ (1 + (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) + (binaryFormRep R w) (MulOpposite.op ↑(ModularGroup.T * ModularGroup.S)) ^ 2).ker

The second exchange map. By the exchange relation ξ (1 + U + U²) ∈ (1 + S) ℛₙ, the action of ξ maps ker (1 + S) into ker (1 + U + U²), where U = T S.

theorem TauCeti.TraceFormulaMatrixModule.ExchangeRelations.periodAction_mem_periodPolynomials {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (hξ : ExchangeRelations R n ξ) {P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)} (hP : P ∈ periodPolynomials R w) : ((periodAction hw) ξ) P ∈ periodPolynomials R w

Popa and Zagier's exchange relations make the determinant-matrix action preserve the period-polynomial space.

noncomputable def TauCeti.TraceFormulaMatrixModule.ExchangeRelations.periodActionRestrict {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (hξ : ExchangeRelations R n ξ) : Module.End R ↥(periodPolynomials R w)

The action of an element satisfying the exchange relations on period polynomials.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.ExchangeRelations.coe_periodActionRestrict_apply {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (hξ : ExchangeRelations R n ξ) (P : ↥(periodPolynomials R w)) : ↑((periodActionRestrict hw hξ) P) = ((periodAction hw) ξ) ↑P

The restricted action agrees with the action on homogeneous forms.

Action of the period relation on the Eisenstein period polynomial

theorem TauCeti.TraceFormulaMatrixModule.periodAction_upperTriangularSum_X_one_pow {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) (n : ℕ) [NeZero n] : ((periodAction hw) (upperTriangularSum R ↑n)) ⟨MvPolynomial.X 1 ^ w, ⋯⟩ = ↑((ArithmeticFunction.sigma (w + 1)) n) • ⟨MvPolynomial.X 1 ^ w, ⋯⟩

The upper-triangular sum Tₙ^∞ (n ≥ 1) scales Y^w by σ_{w+1}(n): for each positive divisor d ∣ n there are d upper-triangular representatives (n/d, b; 0, d) with 0 ≤ b < d, each scaling Y^w by d^w.