The element Tₙ^∞ of the group ring ℛₙ

Popa and Zagier write Tₙ^∞ for the formal sum of the upper-triangular representatives ℳₙ^∞ = TauCeti.TraceFormulaMatrixModule.upperTriangularReps n of Γ \ ℳₙ, an element of the group ring ℛₙ = ℚ[ℳₙ]. This file defines it, over an arbitrary coefficient semiring k, as the element TauCeti.TraceFormulaMatrixModule.upperTriangularSum k n of k[ℳₙ].

Since ℳₙ^∞ is a set of orbit representatives for n ≠ 0, every SL(2, ℤ)-orbit sum of the coefficients of Tₙ^∞ equals 1. Right multiplication by g ∈ PSL(2, ℤ) commutes with the left action, so it permutes the SL(2, ℤ)-orbits, and the orbit sums of the right translate Tₙ^∞ · g are those of Tₙ^∞ permuted; so they equal 1 too. Hence Tₙ^∞ (1 - g) lies in the coinvariant kernel of the left action, which is the input for the existence of a solution of Popa–Zagier's period relation (A). For g = T ^ j more is true: right multiplication by T ^ j keeps matrices upper-triangular, so it permutes the ⟨T⟩-orbits that meet ℳₙ^∞. Hence Tₙ^∞ · T ^ j and Tₙ^∞ have the same ⟨T⟩-orbit sums, and Tₙ^∞ (1 - T ^ j) lies in (1 - T)·k[ℳₙ].

Main definitions

• TauCeti.TraceFormulaMatrixModule.upperTriangularSum k n: the element Tₙ^∞ of k[ℳₙ].

Main results

• TauCeti.TraceFormulaMatrixModule.coeff_upperTriangularSum: Tₙ^∞ is the indicator function of ℳₙ^∞.
• TauCeti.TraceFormulaMatrixModule.upperTriangularSum_eq_sum_reps: Tₙ^∞ as a sum over the matrices of FixedDetMatrices.reps n.
• TauCeti.TraceFormulaMatrixModule.upperTriangularSum_zero: T₀^∞ = 0.
• TauCeti.TraceFormulaMatrixModule.mapDomain_coeff_upperTriangularSum_apply: for n ≠ 0, every SL(2, ℤ)-orbit sum of Tₙ^∞ is 1.
• TauCeti.TraceFormulaMatrixModule.one_sub_ofMulAction_op_upperTriangularSum_mem: Tₙ^∞ (1 - g) lies in the coinvariant kernel of the left action of SL(2, ℤ).
• TauCeti.TraceFormulaMatrixModule.one_sub_ofMulAction_op_T_zpow_upperTriangularSum_mem_range: Tₙ^∞ (1 - T ^ j) lies in (1 - T)·k[ℳₙ].

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 element Tₙ^∞ enters the period relation (A) of §1; that Tₙ^∞ (1 - T) lies in (1 - T)·ℛₙ is used in §3.

noncomputable def TauCeti.TraceFormulaMatrixModule.upperTriangularSum (k : Type u_1) [Semiring k] (n : ℤ) : MonoidAlgebra k (TraceFormulaMatrixModule n)

Popa–Zagier's element Tₙ^∞ of the group ring k[ℳₙ]: the formal sum of the upper-triangular representatives ℳₙ^∞ of Γ \ ℳₙ.

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularSum_def (k : Type u_1) (n : ℤ) [Semiring k] : upperTriangularSum k n = ∑ x ∈ ⋯.toFinset, MonoidAlgebra.single x 1

Definition of Tₙ^∞: the formal sum of the elements of ℳₙ^∞.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.coeff_upperTriangularSum {k : Type u_1} {n : ℤ} [Semiring k] (x : TraceFormulaMatrixModule n) : (upperTriangularSum k n).coeff x = (upperTriangularReps n).indicator 1 x

The coefficients of Tₙ^∞ are the indicator function of ℳₙ^∞.

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularSum_eq_sum_reps (k : Type u_1) (n : ℤ) [Semiring k] : upperTriangularSum k n = ∑ A : ↑(FixedDetMatrices.reps n), MonoidAlgebra.single (mk ↑A) 1

Tₙ^∞ is the sum of the classes of the matrices (a b; 0 d) of FixedDetMatrices.reps n.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.upperTriangularSum_zero {k : Type u_1} [Semiring k] : upperTriangularSum k 0 = 0

T₀^∞ = 0.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mapDomain_coeff_upperTriangularSum_apply {k : Type u_1} {n : ℤ} [Semiring k] (hn : n ≠ 0) (q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) : (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n))) (upperTriangularSum k n).coeff) q = 1

For n ≠ 0, every SL(2, ℤ)-orbit sum of the coefficients of Tₙ^∞ is 1.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mapDomain_coeff_ofMulAction_op_upperTriangularSum_apply {k : Type u_1} {n : ℤ} [Semiring k] (hn : n ≠ 0) (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) (q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n)) : (Finsupp.mapDomain (Quotient.mk (MulAction.orbitRel (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n))) (((Representation.ofMulAction k (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)) (MulOpposite.op g)) (upperTriangularSum k n)).coeff) q = 1

For n ≠ 0 and g ∈ PSL(2, ℤ), every SL(2, ℤ)-orbit sum of the coefficients of the right translate Tₙ^∞ · g is 1.

@[simp]

theorem TauCeti.TraceFormulaMatrixModule.mapDomainLinearMap_ofMulAction_op_T_zpow_upperTriangularSum {k : Type u_1} {n : ℤ} [Semiring k] (j : ℤ) : (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel (↥(Subgroup.zpowers ModularGroup.T)) (TraceFormulaMatrixModule n)))) (((Representation.ofMulAction k (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)) (MulOpposite.op ↑ModularGroup.T ^ j)) (upperTriangularSum k n)) = (MonoidAlgebra.mapDomainLinearMap k k (Quotient.mk (MulAction.orbitRel (↥(Subgroup.zpowers ModularGroup.T)) (TraceFormulaMatrixModule n)))) (upperTriangularSum k n)

For j ∈ ℤ, the ⟨T⟩-orbit sums of the coefficients of the right translate Tₙ^∞ · T ^ j are those of Tₙ^∞.

theorem TauCeti.TraceFormulaMatrixModule.one_sub_ofMulAction_op_upperTriangularSum_mem {k : Type u_1} {n : ℤ} [CommRing k] (g : Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ) : (1 - (Representation.ofMulAction k (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℤ)ᵐᵒᵖ (TraceFormulaMatrixModule n)) (MulOpposite.op g)) (upperTriangularSum k n) ∈ Representation.Coinvariants.ker (Representation.ofMulAction k (Matrix.SpecialLinearGroup (Fin 2) ℤ) (TraceFormulaMatrixModule n))

The right translates of Tₙ^∞ have the same orbit sums. For g ∈ PSL(2, ℤ), the element Tₙ^∞ (1 - g) of k[ℳₙ] lies in the coinvariant kernel of the left action of SL(2, ℤ).

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

The right translates of Tₙ^∞ by powers of T. For j ∈ ℤ, the element Tₙ^∞ (1 - T ^ j) of k[ℳₙ] lies in (1 - T)·k[ℳₙ], the range of left multiplication by 1 - T. Popa–Zagier state the case j = 1; their §3 uses j = ±1.