Evaluating modular symbols at the cusps

Every cusp α ∈ ℙ¹(ℚ) is represented by a primitive integral vector v_α, unique up to sign: (1, 0) for ∞ and (num q, den q) for q ∈ ℚ. For g ∈ SL(2, ℤ) the cusp g∞ is represented by the first column of g. A binary form P of even degree w takes the same value at v and -v, so P(v_α) is a well-defined function of the cusp (TauCeti.ModularSymbols.evalCusp), and it is invariant under SL(2, ℤ): (P ∣ g⁻¹)(v_{gα}) = P(v_α).

Consequently the functional ([α] - [β]) ⊗ P ↦ P(v_α) - P(v_β) on degree-zero divisors tensored with binary forms descends to the modular symbols 𝕄_w(Γ; R) for every Γ ≤ SL(2, ℤ) (TauCeti.ModularSymbols.boundaryEval). It is the boundary map of modular symbols, sending {α, β} ⊗ P to [α] ⊗ P - [β] ⊗ P, followed by the evaluation [α] ⊗ P ↦ P(v_α) on the SL(2, ℤ)-coinvariants of the cusp divisors tensored with binary forms. At level one, the binary form attached to its values on the symbols {∞, 0} ⊗ P is -(X^w - Y^w), the negative of the Eisenstein period polynomial (TauCeti.binaryFormDual_evalCusp_infty_sub_evalCusp_zero, in TauCeti.NumberTheory.ModularForms.LevelOne.TraceFormula.Eisenstein).

Main definitions

• TauCeti.ModularSymbols.evalCusp R w α: the value P ↦ P(v_α) of binary forms at a cusp.
• TauCeti.ModularSymbols.boundaryEval Γ hw: the functional {α, β} ⊗ P ↦ P(v_α) - P(v_β) on 𝕄_w(Γ; R), for even w.

Main results

• TauCeti.ModularSymbols.evalCusp_infty, TauCeti.ModularSymbols.evalCusp_coe: the values at ∞ and at q ∈ ℚ are the values at (1, 0) and at (num q, den q).
• TauCeti.ModularSymbols.evalCusp_mapGL_smul_infty: for even w, the value at g∞ is the value at the first column of g.
• TauCeti.ModularSymbols.evalCusp_mapGL_smul: for even w, (P ∣ g⁻¹)(v_{gα}) = P(v_α).
• TauCeti.ModularSymbols.boundaryEval_mk: the value of the functional on the class of D ⊗ P.
• TauCeti.ModularSymbols.boundaryEval_symbol: the value of the functional on {α, β} ⊗ P.

References

• W. Stein, Modular Forms: A Computational Approach, Graduate Studies in Mathematics 79, American Mathematical Society, 2007, §8.4 (boundary modular symbols).

The primitive vector of a cusp

Binary forms evaluated at the cusps

noncomputable def TauCeti.ModularSymbols.evalCusp (R : Type u_1) [CommRing R] (w : ℕ) (α : OnePoint ℚ) : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w) →ₗ[R] R

The value of a binary form at a cusp: P ↦ P(v_α), where v_α = cuspVector α is the primitive integral vector representing α: (1, 0) for ∞ and (num q, den q) for q ∈ ℚ (TauCeti.ModularSymbols.evalCusp_infty, TauCeti.ModularSymbols.evalCusp_coe). For even w it equals the value at any primitive vector representing α, in particular at the first column of any g ∈ SL(2, ℤ) with g∞ = α (TauCeti.ModularSymbols.evalCusp_mapGL_smul_infty).

@[simp]

theorem TauCeti.ModularSymbols.evalCusp_infty {R : Type u_1} [CommRing R] {w : ℕ} (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (evalCusp R w OnePoint.infty) P = (MvPolynomial.eval ![1, 0]) ↑P

The value at ∞ is the value at (1, 0), the coefficient of Xʷ.

@[simp]

theorem TauCeti.ModularSymbols.evalCusp_coe {R : Type u_1} [CommRing R] {w : ℕ} (q : ℚ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (evalCusp R w ↑q) P = (MvPolynomial.eval ![↑q.num, ↑q.den]) ↑P

The value at q ∈ ℚ is the value at (num q, den q).

theorem TauCeti.ModularSymbols.evalCusp_mapGL_smul_infty {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (evalCusp R w ((Matrix.SpecialLinearGroup.mapGL ℚ) g • OnePoint.infty)) P = (MvPolynomial.eval fun (i : Fin 2) => ↑(↑g i 0)) ↑P

The value at g∞ is the value at the first column of g, for even w.

theorem TauCeti.ModularSymbols.evalCusp_mapGL_smul {R : Type u_1} [CommRing R] {w : ℕ} (hw : Even w) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (α : OnePoint ℚ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (evalCusp R w ((Matrix.SpecialLinearGroup.mapGL ℚ) g • α)) (((binaryFormSLRep R w) g) P) = (evalCusp R w α) P

SL(2, ℤ)-invariance of the values at the cusps. For even w and g ∈ SL(2, ℤ), (P ∣ g⁻¹)(v_{gα}) = P(v_α).

The functional on modular symbols

noncomputable def TauCeti.ModularSymbols.boundaryEval {R : Type u_1} [CommRing R] {w : ℕ} (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hw : Even w) : ModularSymbols R Γ w →ₗ[R] R

Evaluation of modular symbols at the cusps. For even w, the functional on 𝕄_w(Γ; R) sending {α, β} ⊗ P to P(v_α) - P(v_β), where v_α is the primitive integral vector representing α (TauCeti.ModularSymbols.boundaryEval_symbol). It is well defined on the Γ-coinvariants because the values at the cusps are SL(2, ℤ)-invariant (TauCeti.ModularSymbols.evalCusp_mapGL_smul).

@[simp]

theorem TauCeti.ModularSymbols.boundaryEval_mk {R : Type u_1} [CommRing R] {w : ℕ} (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hw : Even w) (D : ↥(degreeZero R)) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (boundaryEval Γ hw) ((Representation.Coinvariants.mk (MonoidHom.comp (symbolRep R w) Γ.subtype)) (D ⊗ₜ[R] P)) = (Finsupp.linearCombination R fun (α : OnePoint ℚ) => (evalCusp R w α) P) (↑D).coeff

On the class of D ⊗ P, the functional boundaryEval is ∑_α D(α) P(v_α).

theorem TauCeti.ModularSymbols.boundaryEval_symbol {R : Type u_1} [CommRing R] {w : ℕ} (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hw : Even w) (α β : OnePoint ℚ) (P : ↥(MvPolynomial.homogeneousSubmodule (Fin 2) R w)) : (boundaryEval Γ hw) ((symbol Γ α β) P) = (evalCusp R w α) P - (evalCusp R w β) P

The functional boundaryEval sends {α, β} ⊗ P to P(v_α) - P(v_β).

theorem TauCeti.ModularSymbols.boundaryEval_comp_symbol {R : Type u_1} [CommRing R] {w : ℕ} (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)) (hw : Even w) (α β : OnePoint ℚ) : boundaryEval Γ hw ∘ₗ symbol Γ α β = evalCusp R w α - evalCusp R w β

On the symbols {α, β} ⊗ P, as a linear map in P, the functional boundaryEval is evalCusp α - evalCusp β.