Traces of linear substitution on binary forms

On homogeneous binary forms of degree w, substitution by any two-by-two matrix has trace dickson 2 (det M) w evaluated at trace M, over any commutative ring. The formula includes matrices with a repeated eigenvalue and does not require diagonalizability. Traces of substitution also commute with changes of coefficient ring, allowing this calculation to descend to fields over which the eigenvalues do not lie.

These are the weight polynomials in the elliptic and hyperbolic terms of the Eichler--Selberg trace formula.

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.trace_linearSubstRep_eq_sum {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommRing R] (w : ℕ) (M : Matrix σ σ R) : (LinearMap.trace R ↥(MvPolynomial.homogeneousSubmodule σ R w)) ((MvPolynomial.linearSubstRep σ R w) (MulOpposite.op M)) = ∑ s ∈ Finset.univ.finsuppAntidiag w, ((MvPolynomial.linearSubst M) ((MvPolynomial.monomial s) 1)).coeff s

The trace of substitution is the sum of the coefficients of each degree-w monomial in its own image.

theorem TauCeti.map_trace_linearSubstRep {σ : Type u_1} {R : Type u_2} {S : Type u_3} [Fintype σ] [DecidableEq σ] [CommRing R] [CommRing S] (w : ℕ) (f : R →+* S) (M : Matrix σ σ R) : f ((LinearMap.trace R ↥(MvPolynomial.homogeneousSubmodule σ R w)) ((MvPolynomial.linearSubstRep σ R w) (MulOpposite.op M))) = (LinearMap.trace S ↥(MvPolynomial.homogeneousSubmodule σ S w)) ((MvPolynomial.linearSubstRep σ S w) (MulOpposite.op (M.map ⇑f)))

Changing the coefficient ring commutes with the trace of homogeneous substitution.

theorem TauCeti.trace_linearSubstRep_upperTriangular {R : Type u_1} [CommRing R] (w : ℕ) (a b d : R) : (LinearMap.trace R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) ((MvPolynomial.linearSubstRep (Fin 2) R w) (MulOpposite.op !![a, b; 0, d])) = Polynomial.eval (a + d) (Polynomial.dickson 2 (a * d) w)

Substitution on binary forms by an upper-triangular matrix has Dickson trace, independently of its upper-right entry.

theorem TauCeti.trace_linearSubstRep_eq_of_isConj {σ : Type u_1} {R : Type u_2} [Fintype σ] [DecidableEq σ] [CommRing R] (w : ℕ) {M N : Matrix σ σ R} (h : IsConj M N) : (LinearMap.trace R ↥(MvPolynomial.homogeneousSubmodule σ R w)) ((MvPolynomial.linearSubstRep σ R w) (MulOpposite.op M)) = (LinearMap.trace R ↥(MvPolynomial.homogeneousSubmodule σ R w)) ((MvPolynomial.linearSubstRep σ R w) (MulOpposite.op N))

The trace of homogeneous substitution is unchanged by conjugating the matrix.

@[simp]

theorem TauCeti.trace_linearSubstRep_eq_dickson_eval {R : Type u_1} [CommRing R] (w : ℕ) (M : Matrix (Fin 2) (Fin 2) R) : (LinearMap.trace R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) ((MvPolynomial.linearSubstRep (Fin 2) R w) (MulOpposite.op M)) = Polynomial.eval M.trace (Polynomial.dickson 2 M.det w)

Over any commutative ring, substitution by a two-by-two matrix on binary forms has Dickson trace. No invertibility or splitting assumption is needed.