Constant terms at the cusps

For an arithmetic subgroup Γ of determinant one (that is, contained in SL₂(ℝ)) and γ ∈ SL₂(ℤ), the constant term of a modular form at the cusp represented by γ is the constant coefficient of the q-expansion of f ∣ γ. We package this as a linear functional. We index by every representative, avoiding a choice of cusp representatives; the common vanishing condition is intrinsic. Bundling all of them gives the linear map ModularForm.constantTerms to SL₂(ℤ) → ℂ.

The constant term at γ depends only on the cusp γ ∞ and on the sign of γ: it is unchanged when γ is multiplied on the left by an element of Γ or on the right by a power of T = [1, 1; 0, 1], and replacing γ by -γ multiplies it by (-1)^k. When Γ contains the principal congruence subgroup Γ(N), which is normal in SL₂(ℤ), it therefore depends only on the bottom row of γ⁻¹ modulo N: for γ = [a, b; c, d] this row is (-c, a), which encodes the cusp a / c modulo N.

The common kernel of these functionals is exactly the cusp-form submodule. Restricting this statement to a nebentypus space identifies the image of S_k(N, χ) inside M_k(N, χ) with the common kernel there. This is the linear-algebraic interface used to compare cusp forms with Eisenstein series through their constant terms.

Main definitions

• ModularForm.constantTermAt: the constant-term functional attached to an element of SL₂(ℤ).
• ModularForm.constantTerms: all constant terms at once, as a linear map to SL₂(ℤ) → ℂ.

Main results

• ModularForm.tendsto_translate_constantTermAt: f ∣ γ tends to the constant term at i∞.
• ModularForm.constantTermAt_mul_left, ModularForm.constantTermAt_mul_T_zpow, ModularForm.constantTermAt_neg: the dependence of the constant term on the representative.
• ModularForm.constantTermAt_eq_of_vecMul_inv_eq: on a group containing Γ(N), the constant term at γ depends only on the bottom row of γ⁻¹ modulo N.
• ModularForm.mem_cuspFormSubmodule_iff_constantTermAt_eq_zero: a modular form is cuspidal if and only if every translated constant term vanishes.
• ModularForm.ker_constantTerms: the kernel of constantTerms is the cusp-form submodule.
• TauCeti.mem_range_cuspToModFormCharSpace_iff_constantTermAt_eq_zero: the same characterization inside a nebentypus space.
• TauCeti.range_cuspToModFormCharSpace_eq_ker_constantTerms: the image of S_k(N, χ) in M_k(N, χ) is the kernel of constantTerms restricted to M_k(N, χ).

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, §3.1.

noncomputable def ModularForm.constantTermAt {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : ModularForm Γ k →ₗ[ℂ] ℂ

The constant term of f at the cusp represented by γ ∈ SL₂(ℤ), as a linear functional.

It is the constant coefficient after translating by γ. The q-expansion uses the canonical strict width at infinity of the conjugated arithmetic subgroup.

Equations

• ModularForm.constantTermAt γ = PowerSeries.coeff 0 ∘ₗ TauCeti.ModularForm.qExpansionLinearMap ⋯ ⋯ k ∘ₗ ModularForm.translateₗ ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) ⋯

@[simp]

theorem ModularForm.constantTermAt_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ModularForm Γ k) : (constantTermAt γ) f = (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion (ConjAct.toConjAct ((Matrix.SpecialLinearGroup.mapGL ℝ) γ)⁻¹ • Γ).strictWidthInfty ⇑(translate f ((Matrix.SpecialLinearGroup.mapGL ℝ) γ)))

The constant-term functional evaluates to the constant coefficient of the translated q-expansion.

theorem ModularForm.constantTermAt_eq_valueAtInfty {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ModularForm Γ k) : (constantTermAt γ) f = UpperHalfPlane.valueAtInfty ⇑(translate f ((Matrix.SpecialLinearGroup.mapGL ℝ) γ))

The constant term is the value at infinity of the translated modular form.

theorem ModularForm.tendsto_translate_constantTermAt {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ModularForm Γ k) : Filter.Tendsto (⇑(translate f ((Matrix.SpecialLinearGroup.mapGL ℝ) γ))) UpperHalfPlane.atImInfty (nhds ((constantTermAt γ) f))

The translate f ∣ γ tends to the constant term of f at γ at i∞.

theorem ModularForm.constantTermAt_mul_left {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] {h : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hh : (Matrix.SpecialLinearGroup.mapGL ℝ) h ∈ Γ) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ModularForm Γ k) : (constantTermAt (h * γ)) f = (constantTermAt γ) f

Multiplying the representative on the left by an element of Γ does not change the constant term.

theorem ModularForm.constantTermAt_mul_T_zpow {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (j : ℤ) (f : ModularForm Γ k) : (constantTermAt (γ * ModularGroup.T ^ j)) f = (constantTermAt γ) f

Multiplying the representative on the right by a power of T does not change the constant term, since slashing by T ^ j is the translation τ ↦ τ + j.

theorem ModularForm.constantTermAt_neg {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (f : ModularForm Γ k) : (constantTermAt (-γ)) f = (-1) ^ k * (constantTermAt γ) f

Negating the representative multiplies the constant term by (-1)^k.

theorem ModularForm.mem_cuspFormSubmodule_iff_constantTermAt_eq_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (f : ModularForm Γ k) : f ∈ cuspFormSubmodule Γ k ↔ ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (constantTermAt γ) f = 0

A modular form is cuspidal exactly when its constant term vanishes after every SL₂(ℤ)-translate.

noncomputable def ModularForm.constantTerms {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] : ModularForm Γ k →ₗ[ℂ] Matrix.SpecialLinearGroup (Fin 2) ℤ → ℂ

All constant terms at once: the linear map sending f to γ ↦ constantTermAt γ f.

Equations

• ModularForm.constantTerms = LinearMap.pi ModularForm.constantTermAt

@[simp]

theorem ModularForm.constantTerms_apply {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] (f : ModularForm Γ k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : constantTerms f γ = (constantTermAt γ) f

theorem ModularForm.ker_constantTerms {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] : constantTerms.ker = cuspFormSubmodule Γ k

The common kernel of the constant-term functionals is the cusp-form submodule.

theorem ModularForm.constantTermAt_eq_of_vecMul_inv_eq {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.HasDetOne] [Γ.IsArithmetic] {N : ℕ} (hΓ : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N) ≤ Γ) {γ₁ γ₂ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (h : Matrix.vecMul ![0, 1] ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ₁⁻¹) = Matrix.vecMul ![0, 1] ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ₂⁻¹)) (f : ModularForm Γ k) : (constantTermAt γ₁) f = (constantTermAt γ₂) f

If Γ contains Γ(N), the constant term at γ depends only on the bottom row of γ⁻¹ modulo N. For γ = [a, b; c, d] that row is (-c, a), so the constant term depends only on the cusp a / c modulo N.

theorem TauCeti.mem_range_cuspToModFormCharSpace_iff_constantTermAt_eq_zero {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (f : ↥(modFormCharSpace k χ)) : f ∈ (cuspToModFormCharSpace k χ).range ↔ ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ), (ModularForm.constantTermAt γ) ↑f = 0

Inside M_k(N, χ), the common kernel of the cusp constant terms is precisely the image of S_k(N, χ).

theorem TauCeti.range_cuspToModFormCharSpace_eq_ker_constantTerms {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} : (cuspToModFormCharSpace k χ).range = (ModularForm.constantTerms ∘ₗ (modFormCharSpace k χ).subtype).ker

The image of S_k(N, χ) in M_k(N, χ) is the kernel of the constant terms restricted to M_k(N, χ).