Documentation

TauCeti.NumberTheory.ModularForms.Cusps.LevelRaise

Constant terms under level raising #

At the cusp represented by γ = [a,b;c,d], the degeneracy map V_t f(z) = f(tz) multiplies the constant term at the reduced cusp ta/c by (gcd(c,t)/t)^k. The formula uses any integral determinant-one representative whose first column is (ta/g, c/g), where g = gcd(c,t); hence it involves no choice of a preferred representative. It applies to modular forms for arbitrary arithmetic determinant-one subgroups with the level-raising inclusion. This transports constant-term vectors of Eisenstein series to higher levels.

The two matrix reductions also apply to functions with a transformation law, such as the quasimodular weight-two Eisenstein series.

References #

theorem Matrix.SpecialLinearGroup.exists_scaled_cusp_reduction (γ : SpecialLinearGroup (Fin 2) ℤ) {t : ℕ} [NeZero t] :
∃ (δ : SpecialLinearGroup (Fin 2) ℤ), ↑t * ↑γ 0 0 = ↑δ 0 0 * ↑((↑γ 1 0).gcd ↑t) ∧ ↑γ 1 0 = ↑δ 1 0 * ↑((↑γ 1 0).gcd ↑t)

A representative of the scaled cusp with primitive first column.

theorem Matrix.SpecialLinearGroup.scaled_cusp_upperTriangular (γ δ : SpecialLinearGroup (Fin 2) ℤ) {t : ℕ} [NeZero t] (ha : ↑t * ↑γ 0 0 = ↑δ 0 0 * ↑((↑γ 1 0).gcd ↑t)) (hc : ↑γ 1 0 = ↑δ 1 0 * ↑((↑γ 1 0).gcd ↑t)) :
have β := ((mapGL ℝ) δ)⁻¹ * (TauCeti.scaleGL t * (mapGL ℝ) γ); ↑β 1 0 = 0 ∧ ↑β 1 1 = ↑t / ↑((↑γ 1 0).gcd ↑t)

Reducing the scaled cusp leaves an upper-triangular factor with lower-right entry t / gcd(c,t).

theorem ModularForm.constantTermAt_levelRaise {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetOne] [Γ.IsArithmetic] [Γ'.HasDetOne] [Γ'.IsArithmetic] {k : ℤ} {t : ℕ} [NeZero t] (f : ModularForm Γ k) (h : Γ' ≤ ConjAct.toConjAct (TauCeti.scaleGL t)⁻¹ • Γ) (γ δ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (ha : ↑t * ↑γ 0 0 = ↑δ 0 0 * ↑((↑γ 1 0).gcd ↑t)) (hc : ↑γ 1 0 = ↑δ 1 0 * ↑((↑γ 1 0).gcd ↑t)) :
(constantTermAt γ) (TauCeti.ModularForm.levelRaise t h f) = (↑((↑γ 1 0).gcd ↑t) / ↑t) ^ k * (constantTermAt δ) f

Constant-term transport under level raising. If δ represents the reduced cusp ta/c, then the constant term of V_t f at a/c is (gcd(c,t)/t)^k times that of f at δ. The first-column equations fix the sign of the representative, including in odd weight.