Documentation

TauCeti.NumberTheory.ModularForms.LevelOne.TraceFormula.HeckeSymbol

Solutions of the period relation act as Hecke operators #

Let ℳₙ be the projective determinant-n matrix module and ℛₙ = R[ℳₙ]. An element ξ = ∑ c_M M of ℛₙ sends a binary form P of even degree w to the level-one modular symbol

∑ c_M {∞, 0} ⊗ (P ∣ adj M) ∈ 𝕄_w(SL(2, ℤ); R)

(TauCeti.TraceFormulaMatrixModule.symbolAction), where P ∣ adj M is the adjugate substitution. Through the duality TauCeti.binaryFormDual between binary forms and functionals on them, this is the transpose of the substitution action TauCeti.TraceFormulaMatrixModule.periodAction of ξ on period polynomials (TauCeti.TraceFormulaMatrixModule.periodAction_binaryFormDual).

Popa and Zagier's Proposition 2 says that every solution ξ of the period relation (A) (1 - S)·ξ - Tₙ^∞·(1 - S) ∈ (1 - T)·ℛₙ acts on period polynomials as the classical Hecke operator Tₙ. On modular symbols this is the identity

∑ c_M {∞, 0} ⊗ (P ∣ adj M) = ∑_{(a b; 0 d) ∈ ℳₙ^∞} {∞, b/d} ⊗ (P ∣ adj (a b; 0 d))

(TauCeti.TraceFormulaMatrixModule.PeriodRelation.symbolAction_eq). Its right-hand side TauCeti.TraceFormulaMatrixModule.upperTriangularSymbol is ∑ {a∞, a0} ⊗ (P ∣ adj a), the sum of the translates of {∞, 0} ⊗ P by the upper-triangular representatives a = (a b; 0 d) of Γ \ ℳₙ; for n > 0 these are the matrices with ad = n, a > 0 and 0 ≤ b < d. For n > 0 this is the classical Hecke operator Tₙ applied to {∞, 0} ⊗ P, which runs over all determinant-n double cosets Γ diag(a, d) Γ with a ∣ d. Identifying it with the sum of the double-coset operators TauCeti.ModularSymbols.heckeSymbol over these cosets is not proved here; for non-squarefree n this sum has more terms than the single double coset Γ diag(1, n) Γ of TauCeti.ModularSymbols.heckeTSymbol.

The proof applies to the relation (A) the linear map M ↦ {∞, M0} ⊗ (P ∣ adj M). Left multiplication by g ∈ SL(2, ℤ) replaces its value by {g⁻¹∞, M0} ⊗ (P ∣ adj M). For g = T nothing changes, so the map kills (1 - T)·ℛₙ; for g = S the value drops by {∞, 0} ⊗ (P ∣ adj M), so the map sends (1 - S)·ξ to the action of ξ. It sends Tₙ^∞ to the right-hand side above and kills Tₙ^∞·S, since (a S)0 = a∞ = ∞ for upper-triangular a.

The period map of a level-one cusp form f is a functional on 𝕄_w(SL(2, ℤ); ℂ), and the binary form attached to its restriction to the symbols {∞, 0} ⊗ P is the period polynomial r_f. So TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_binaryFormDual expresses the action of ξ on r_f through the periods of f on the symbols ∑ {a∞, a0} ⊗ (P ∣ adj a). The substitution z ↦ a z turns these into the periods of the slashes f ∣[k] a on {∞, 0}, whose sum is the classical Hecke transform Tₙ f = TauCeti.heckeTCuspLevelOne k n f. Hence r_f ∣ ξ = r_{Tₙ f} for every n ≥ 1 (TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_periodPolynomial).

Main definitions #

Main results #

References #

The action of ℛₙ on the Manin symbol {∞, 0} #

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

The action of ℛₙ on the Manin symbol {∞, 0}. An element ξ = ∑ c_M M of R[ℳₙ] sends a binary form P of even degree w to ∑ c_M {∞, 0} ⊗ (P ∣ adj M) in the level-one modular symbols. Under the duality between binary forms and functionals it is the transpose of the substitution action TauCeti.TraceFormulaMatrixModule.periodAction (TauCeti.TraceFormulaMatrixModule.periodAction_binaryFormDual).

Instances For
    source
    @[simp]
    theorem TauCeti.TraceFormulaMatrixModule.symbolAction_single {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (A : TraceFormulaMatrix n) (c : R) :
    (symbolAction hw) (MonoidAlgebra.single (mk A) c) = c • ModularSymbols.symbol ⊤ OnePoint.infty ↑0 ∘ₗ (binaryFormAdjugateRep R w) ↑A

    A basis element c • [M] acts by P ↦ c • {∞, 0} ⊗ (P ∣ adj M).

    source
    theorem TauCeti.TraceFormulaMatrixModule.periodAction_binaryFormDual {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hw : Even w) (ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)) (φ : ModularSymbols R ⊤ w →ₗ[R] R) :
    ((periodAction hw) ξ) ((binaryFormDual R w) (φ ∘ₗ ModularSymbols.symbol ⊤ OnePoint.infty ↑0)) = (binaryFormDual R w) (φ ∘ₗ (symbolAction hw) ξ)

    The action on modular symbols is the transpose of the action on binary forms. For a functional φ on the level-one modular symbols, the substitution action of ξ on the binary form attached to P ↦ φ ({∞, 0} ⊗ P) is the binary form attached to φ ∘ symbolAction ξ. For φ the period map of a cusp form f, the former binary form is the period polynomial r_f.

    The sum over the upper-triangular representatives #

    source
    noncomputable def TauCeti.TraceFormulaMatrixModule.upperTriangularSymbol (R : Type u_1) [CommRing R] (n : ℤ) (w : ℕ) :
    ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] ModularSymbols R ⊤ w

    The sum over the upper-triangular representatives of Γ \ ℳₙ: the map sending a binary form P to ∑ {∞, b/d} ⊗ (P ∣ adj (a b; 0 d)), the sum over FixedDetMatrices.reps n. Each summand is the translate {a∞, a0} ⊗ (P ∣ adj a) of {∞, 0} ⊗ P by a = (a b; 0 d). For n > 0 this is the classical Hecke operator Tₙ, over all determinant-n double cosets, applied to {∞, 0} ⊗ P; its identification with TauCeti.ModularSymbols.heckeSymbol is not proved here.

    Instances For
      source
      theorem TauCeti.TraceFormulaMatrixModule.upperTriangularSymbol_apply {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) :
      (upperTriangularSymbol R n w) P = ∑ A : ↑(FixedDetMatrices.reps n), (ModularSymbols.symbol ⊤ OnePoint.infty ↑(↑(↑↑A 0 1) / ↑(↑↑A 1 1))) (((binaryFormAdjugateRep R w) ↑↑A) P)

      The value of upperTriangularSymbol R n w at P is ∑ {∞, b/d} ⊗ (P ∣ adj (a b; 0 d)).

      The auxiliary map M ↦ {∞, M0} ⊗ (P ∣ adj M) #

      source
      theorem TauCeti.TraceFormulaMatrixModule.upperTriangularSymbol_eq_sum_toGL_smul {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hn : n ≠ 0) :
      upperTriangularSymbol R n w = ∑ A : ↑(FixedDetMatrices.reps n), ModularSymbols.symbol ⊤ (FixedDetMatrices.toGL hn ↑A • OnePoint.infty) (FixedDetMatrices.toGL hn ↑A • ↑0) ∘ₗ (binaryFormAdjugateRep R w) ↑↑A

      The sum over ℳₙ^∞ as a sum of translates. For n ≠ 0, upperTriangularSymbol R n w sends P to ∑ {a∞, a0} ⊗ (P ∣ adj a), the sum over the upper-triangular representatives a of Γ \ ℳₙ acting on the cusps through FixedDetMatrices.toGL.

      Popa–Zagier's Proposition 2 on modular symbols #

      source
      theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.symbolAction_eq {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hn : n ≠ 0) (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (h : PeriodRelation R n ξ) :
      (symbolAction hw) ξ = upperTriangularSymbol R n w

      Popa–Zagier, Proposition 2, on modular symbols. For n ≠ 0, every solution ξ = ∑ c_M M of the period relation (A) satisfies

      ∑ c_M {∞, 0} ⊗ (P ∣ adj M) = ∑_{(a b; 0 d)} {∞, b/d} ⊗ (P ∣ adj (a b; 0 d)),

      the sum upperTriangularSymbol R n w on the right running over the upper-triangular representatives FixedDetMatrices.reps n of Γ \ ℳₙ, on which (a b; 0 d) sends ∞ to ∞ and 0 to b/d.

      source
      theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_binaryFormDual {R : Type u_1} [CommRing R] {n : ℤ} {w : ℕ} (hn : n ≠ 0) (hw : Even w) {ξ : MonoidAlgebra R (TraceFormulaMatrixModule n)} (h : PeriodRelation R n ξ) (φ : ModularSymbols R ⊤ w →ₗ[R] R) :
      ((periodAction hw) ξ) ((binaryFormDual R w) (φ ∘ₗ ModularSymbols.symbol ⊤ OnePoint.infty ↑0)) = (binaryFormDual R w) (φ ∘ₗ upperTriangularSymbol R n w)

      Popa–Zagier, Proposition 2. Let n ≠ 0, let ξ be a solution of the period relation (A), and let φ be a functional on the level-one modular symbols. The substitution action of ξ on the binary form attached to P ↦ φ ({∞, 0} ⊗ P) is the binary form attached to φ ∘ upperTriangularSymbol R n w, that is, to P ↦ φ (∑ {∞, b/d} ⊗ (P ∣ adj (a b; 0 d))), the sum over the upper-triangular representatives (a b; 0 d) of Γ \ ℳₙ. For φ the period map of a level-one cusp form f, the former binary form is the period polynomial r_f.

      Popa–Zagier's Proposition 2 on period polynomials of cusp forms #

      source
      theorem TauCeti.TraceFormulaMatrixModule.PeriodRelation.periodAction_periodPolynomial {w : ℕ} {k : ℤ} (hk : k = ↑w + 2) (hw : Even w) (n : ℕ) [NeZero n] {ξ : MonoidAlgebra ℂ (TraceFormulaMatrixModule ↑n)} (h : PeriodRelation ℂ (↑n) ξ) (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) :
      ((periodAction hw) ξ) ↑((periodPolynomial hk) f) = ↑((periodPolynomial hk) ((heckeTCuspLevelOne k n) f))

      Popa–Zagier, Proposition 2, on period polynomials. Let n ≥ 1 and let ξ be a solution of the period relation (A). For every level-one cusp form f of weight w + 2, the action of ξ on the period polynomial of f is the period polynomial of the Hecke transform:

      r_f ∣ ξ = r_{Tₙ f},

      with Tₙ = TauCeti.heckeTCuspLevelOne (w + 2) n the classical Hecke operator, the sum over all of SL(2, ℤ) \ ℳₙ.