Binary-form traces for arbitrary determinant matrices

Every integral matrix acts on binary forms over any commutative ring with trace P_{w+2}(trace M, det M), expressed using the Dickson polynomial dickson 2 (det M) w. This applies to elliptic and nonsplit hyperbolic matrices, as well as to triangular and scalar matrices. On even-degree forms it descends to the projective determinant-matrix module.

The linear extension expresses the ambient trace of any finite determinant-matrix sum as the sum of its coefficients times these weight polynomials. This permits grouping the trace by conjugacy classes, without a rational diagonalization assumption.

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, Section 4.

theorem TauCeti.TraceFormulaMatrixModule.trace_binaryFormAction_eq_dickson_eval {n : ℤ} {K : Type u_1} [CommRing K] (w : ℕ) (hw : Even w) (A : TraceFormulaMatrix n) : (LinearMap.trace K ↥(MvPolynomial.homogeneousSubmodule (Fin 2) K w)) (binaryFormAction hw (mk A)) = Polynomial.eval (↑(↑A).trace) (Polynomial.dickson 2 (↑n) w)

A projective matrix has Dickson trace on even-degree binary forms over any commutative ring.

theorem TauCeti.TraceFormulaMatrixModule.trace_periodAction_single_eq_dickson_eval {n : ℤ} {K : Type u_1} [CommRing K] (w : ℕ) (hw : Even w) (A : TraceFormulaMatrix n) (c : K) : (LinearMap.trace K ↥(MvPolynomial.homogeneousSubmodule (Fin 2) K w)) ((periodAction hw) (MonoidAlgebra.single (mk A) c)) = c * Polynomial.eval (↑(↑A).trace) (Polynomial.dickson 2 (↑n) w)

A determinant-matrix basis element contributes its coefficient times the Dickson weight polynomial to the trace of its action.

theorem TauCeti.TraceFormulaMatrixModule.trace_periodAction_sum_eq_dickson_eval {n : ℤ} {K : Type u_1} [CommRing K] (w : ℕ) (hw : Even w) (s : Finset (TraceFormulaMatrix n)) (c : TraceFormulaMatrix n → K) : (LinearMap.trace K ↥(MvPolynomial.homogeneousSubmodule (Fin 2) K w)) ((periodAction hw) (∑ A ∈ s, MonoidAlgebra.single (mk A) (c A))) = ∑ A ∈ s, c A * Polynomial.eval (↑(↑A).trace) (Polynomial.dickson 2 (↑n) w)

The trace of a finite sum of determinant-matrix basis elements is the corresponding coefficient-weighted sum of Dickson polynomials. Representatives need not be distinct modulo sign.