The action of integral matrices on binary forms

Fix a commutative ring R and a natural number w. Let V_w be the R-module of binary forms of degree w, modelled as homogeneousSubmodule (Fin 2) R w with X = X 0 and Y = X 1. Integral 2 × 2 matrices act on it on the right, (P ∣ M)(X, Y) = P(aX + bY, cX + dY) for M = !![a, b; c, d], so that P ∣ (M * N) = (P ∣ M) ∣ N. This action is the coefficient module of both period polynomials and modular symbols of weight w + 2.

A linear functional φ on V_w determines the binary form D φ whose value at (x, y) is φ ((xY - yX)ʷ). This construction is compatible with the actions: the action of M on D φ is the adjugate action on φ, transposed. Applied to the period functional P ↦ ∫₀^{i∞} f(τ) P(τ, 1) dτ of a cusp form f, it produces the period polynomial r_f(X, Y) = ∫₀^{i∞} f(τ) (X - τY)ʷ dτ.

Main definitions

• TauCeti.binaryFormRep R w: the right action of integral matrices on binary forms of degree w, as a representation of (Matrix (Fin 2) (Fin 2) ℤ)ᵐᵒᵖ.
• TauCeti.binaryFormAdjugateRep R w: the left action P ↦ P ∣ adj M of integral matrices, the right action precomposed with the anti-multiplicative adjugate.
• TauCeti.binaryFormMonomialBasis R w: the monomial basis Xʲ Yʷ⁻ʲ, 0 ≤ j ≤ w.
• TauCeti.linearFormPow R w x y: the binary form (xY - yX)ʷ.
• TauCeti.binaryFormDual R w: the linear map φ ↦ D φ from functionals to binary forms.

Main results

• TauCeti.binaryFormRep_op_mul_apply: the action is on the right, P ∣ (M * N) = (P ∣ M) ∣ N.
• TauCeti.binaryFormRep_op_neg, TauCeti.binaryFormRep_op_scalar: negated and scalar matrices act by (-1)ʷ and by the wth power of the scalar.
• TauCeti.mapHomogeneousSubmodule_binaryFormRep: changing coefficients commutes with the action.
• TauCeti.trace_binaryFormRep_eq_dickson_eval: the trace is the Dickson weight polynomial evaluated at the matrix trace and determinant.
• TauCeti.binaryFormRep_adjugate_linearFormPow: (xY - yX)ʷ ∣ adj M = (x'Y - y'X)ʷ for (x', y') = M (x, y).
• TauCeti.eval_binaryFormDual: D φ takes the value φ ((xY - yX)ʷ) at (x, y).
• TauCeti.binaryFormRep_binaryFormDual: (D φ) ∣ M = D (φ ∘ (· ∣ adj M)).
• TauCeti.binaryFormDual_injective: D is injective when the binomial coefficients w choose j are not zero divisors.

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.

noncomputable def TauCeti.binaryFormRep (R : Type u_1) [CommRing R] (w : ℕ) : Representation R (Matrix (Fin 2) (Fin 2) ℤ)ᵐᵒᵖ ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The right action P ↦ P ∣ M of integral 2 × 2 matrices on binary forms of degree w, (P ∣ M)(X, Y) = P(aX + bY, cX + dY) for M = !![a, b; c, d], as a representation of the opposite matrix monoid.

Equations

• TauCeti.binaryFormRep R w = MonoidHom.comp (MvPolynomial.linearSubstRep (Fin 2) R w) (MonoidHom.op ↑(Int.castRingHom R).mapMatrix)

theorem TauCeti.binaryFormRep_op {R : Type u_1} [CommRing R] {w : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) : (binaryFormRep R w) (MulOpposite.op M) = (MvPolynomial.linearSubstRep (Fin 2) R w) (MulOpposite.op (M.map ⇑(Int.castRingHom R)))

Integral substitution is homogeneous substitution after mapping the matrix entries into its coefficient ring.

theorem TauCeti.trace_binaryFormRep_eq_dickson_eval {K : Type u_2} [CommRing K] (w : ℕ) (M : Matrix (Fin 2) (Fin 2) ℤ) : (LinearMap.trace K ↥(MvPolynomial.homogeneousSubmodule (Fin 2) K w)) ((binaryFormRep K w) (MulOpposite.op M)) = Polynomial.eval (↑M.trace) (Polynomial.dickson 2 (↑M.det) w)

The trace of an integral matrix on binary forms is its Dickson weight polynomial.

@[simp]

theorem TauCeti.coe_binaryFormRep_apply {R : Type u_1} [CommRing R] {w : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : ↑(((binaryFormRep R w) (MulOpposite.op M)) P) = (MvPolynomial.linearSubst (M.map Int.cast)) ↑P

theorem TauCeti.binaryFormRep_op_mul_apply {R : Type u_1} [CommRing R] {w : ℕ} (M N : Matrix (Fin 2) (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : ((binaryFormRep R w) (MulOpposite.op (M * N))) P = ((binaryFormRep R w) (MulOpposite.op N)) (((binaryFormRep R w) (MulOpposite.op M)) P)

The action is on the right: P ∣ (M * N) = (P ∣ M) ∣ N.

theorem TauCeti.binaryFormRep_op_neg {R : Type u_1} [CommRing R] {w : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) : (binaryFormRep R w) (MulOpposite.op (-M)) = (-1) ^ w • (binaryFormRep R w) (MulOpposite.op M)

Negating the matrix multiplies a form of degree w by (-1)ʷ.

theorem TauCeti.binaryFormRep_op_neg_of_even {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) (M : Matrix (Fin 2) (Fin 2) ℤ) : (binaryFormRep R w) (MulOpposite.op (-M)) = (binaryFormRep R w) (MulOpposite.op M)

For even w, a matrix and its negative act in the same way.

noncomputable def TauCeti.binaryFormAdjugateRep (R : Type u_1) [CommRing R] (w : ℕ) : Representation R (Matrix (Fin 2) (Fin 2) ℤ) ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The left action P ↦ P ∣ adj M of integral matrices on binary forms of degree w, as a representation of the matrix monoid: the adjugate is anti-multiplicative, so precomposing the right action TauCeti.binaryFormRep with it gives a left action. On SL(2, ℤ) the adjugate is the inverse, so this restricts to P ↦ P ∣ γ⁻¹; on a matrix of determinant n it is the action that appears in the Hecke operators on modular symbols, where {α, β} ⊗ P is sent to {δα, δβ} ⊗ (P ∣ adj δ).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.binaryFormAdjugateRep_apply {R : Type u_1} [CommRing R] {w : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : ((binaryFormAdjugateRep R w) M) P = ((binaryFormRep R w) (MulOpposite.op M.adjugate)) P

@[simp]

theorem TauCeti.binaryFormRep_op_scalar {R : Type u_1} [CommRing R] {w : ℕ} (a : ℤ) : (binaryFormRep R w) (MulOpposite.op !![a, 0; 0, a]) = ↑a ^ w • 1

An integer scalar matrix acts on degree-w binary forms by its wth power.

Binary forms attached to linear functionals

noncomputable def TauCeti.binaryFormMonomialBasis (R : Type u_2) [CommSemiring R] (w : ℕ) : Module.Basis (Fin (w + 1)) R ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The monomial basis Xʲ Yʷ⁻ʲ, 0 ≤ j ≤ w, of the binary forms of degree w, indexed by the exponent j of X.

Equations

• TauCeti.binaryFormMonomialBasis R w = (TauCeti.homogeneousMonomialBasis w).reindex (TauCeti.finsuppDegreeFinTwoEquiv w)

@[simp]

theorem TauCeti.coe_binaryFormMonomialBasis {R : Type u_2} [CommSemiring R] {w : ℕ} (j : Fin (w + 1)) : ↑((binaryFormMonomialBasis R w) j) = MvPolynomial.X 0 ^ ↑j * MvPolynomial.X 1 ^ (w - ↑j)

@[simp]

theorem TauCeti.mapHomogeneousSubmodule_binaryFormMonomialBasis {w : ℕ} {S : Type u_2} {R : Type u_3} [CommSemiring S] [CommSemiring R] (f : S →+* R) (j : Fin (w + 1)) : (mapHomogeneousSubmodule f w) ((binaryFormMonomialBasis S w) j) = (binaryFormMonomialBasis R w) j

Changing coefficients sends the monomial basis to the monomial basis.

theorem TauCeti.mapHomogeneousSubmodule_binaryFormRep {R : Type u_1} [CommRing R] {w : ℕ} {S : Type u_2} [CommRing S] (f : S →+* R) (M : Matrix (Fin 2) (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) S w)) : (mapHomogeneousSubmodule f w) (((binaryFormRep S w) (MulOpposite.op M)) P) = ((binaryFormRep R w) (MulOpposite.op M)) ((mapHomogeneousSubmodule f w) P)

Changing coefficients commutes with the action of integral matrices.

noncomputable def TauCeti.linearFormPow (R : Type u_1) [CommRing R] (w : ℕ) (x y : R) : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The binary form (xY - yX)ʷ of degree w, the wth power of a linear form vanishing at (x, y). Its value at (τ, 1) is (x - yτ)ʷ.

Equations

• TauCeti.linearFormPow R w x y = ⟨(MvPolynomial.C x * MvPolynomial.X 1 - MvPolynomial.C y * MvPolynomial.X 0) ^ w, ⋯⟩

@[simp]

theorem TauCeti.coe_linearFormPow {R : Type u_1} [CommRing R] {w : ℕ} (x y : R) : ↑(linearFormPow R w x y) = (MvPolynomial.C x * MvPolynomial.X 1 - MvPolynomial.C y * MvPolynomial.X 0) ^ w

theorem TauCeti.linearFormPow_eq_sum {R : Type u_1} [CommRing R] {w : ℕ} (x y : R) : linearFormPow R w x y = ∑ j : Fin (w + 1), (↑(w.choose ↑j) * (-y) ^ ↑j * x ^ (w - ↑j)) • (binaryFormMonomialBasis R w) j

The binomial expansion of (xY - yX)ʷ in the monomial basis.

theorem TauCeti.binaryFormRep_adjugate_linearFormPow {R : Type u_1} [CommRing R] {w : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) (v : Fin 2 → R) : ((binaryFormRep R w) (MulOpposite.op M.adjugate)) (linearFormPow R w (v 0) (v 1)) = linearFormPow R w ((M.map Int.cast).mulVec v 0) ((M.map Int.cast).mulVec v 1)

Substituting the adjugate of M into (xY - yX)ʷ gives (x'Y - y'X)ʷ, where (x', y') = M (x, y).

noncomputable def TauCeti.binaryFormDual (R : Type u_1) [CommRing R] (w : ℕ) : (↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] R) →ₗ[R] ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)

The binary form attached to a functional. A linear functional φ on the binary forms of degree w determines the binary form D φ whose value at (x, y) is φ ((xY - yX)ʷ) (TauCeti.eval_binaryFormDual). Explicitly, D φ = ∑ⱼ (-1)ʷ⁻ʲ (w choose j) φ (Xʷ⁻ʲ Yʲ) Xʲ Yʷ⁻ʲ. For the period functional P ↦ ∫₀^{i∞} f(τ) P(τ, 1) dτ of a cusp form f this is the period polynomial r_f(X, Y) = ∫₀^{i∞} f(τ) (X - τY)ʷ dτ.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.binaryFormDual_apply {R : Type u_1} [CommRing R] {w : ℕ} (φ : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] R) : (binaryFormDual R w) φ = ∑ j : Fin (w + 1), ((-1) ^ (w - ↑j) * ↑(w.choose ↑j) * φ ((binaryFormMonomialBasis R w) j.rev)) • (binaryFormMonomialBasis R w) j

@[simp]

theorem TauCeti.eval_binaryFormDual {R : Type u_1} [CommRing R] {w : ℕ} (φ : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] R) (v : Fin 2 → R) : (MvPolynomial.eval v) ↑((binaryFormDual R w) φ) = φ (linearFormPow R w (v 0) (v 1))

The value of D φ at (x, y) is φ ((xY - yX)ʷ).

theorem TauCeti.binaryFormRep_binaryFormDual {R : Type u_1} [CommRing R] {w : ℕ} (M : Matrix (Fin 2) (Fin 2) ℤ) (φ : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] R) : ((binaryFormRep R w) (MulOpposite.op M)) ((binaryFormDual R w) φ) = (binaryFormDual R w) (φ ∘ₗ (binaryFormAdjugateRep R w) M)

Equivariance of D. For every integral matrix M, (D φ) ∣ M = D (φ ∘ (· ∣ adj M)): the action of Mon the binary form attached toφ` is the transpose of the adjugate action on the functional.

theorem TauCeti.binaryFormDual_injective {R : Type u_1} [CommRing R] {w : ℕ} (h : ∀ j ≤ w, IsRegular ↑(w.choose j)) : Function.Injective ⇑(binaryFormDual R w)

D is injective when the binomial coefficients w choose j are not zero divisors, for instance over a domain of characteristic zero or of characteristic p > w.