Cusp forms of nonpositive weight for a finite-index subgroup of $\mathrm{SL}_2(\mathbb Z)$ vanish

Proved

MTT.eq_zero_of_slash_invariant_of_weight_nonpos

by cbirkbeck · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsnumber-theory

Let $\Gamma \le \mathrm{SL}_2(\mathbb Z)$ be a subgroup of finite index and let $w \le 0$ be an integer. Let $F : \mathfrak H \to \mathbb C$ be holomorphic, invariant under $\Gamma$ in weight $w$ , i.e.

F(\gamma z) = (cz+d)^{w} F(z) \qquad \text{for all } \gamma = \begin{pmatrix} a & b \\ c & d \end{pmatrix} \in \Gamma,

and vanishing at every cusp, in the sense that $(F|_w g)(z) \to 0$ as $\operatorname{Im} z \to \infty$ for every $g \in \mathrm{SL}_2(\mathbb Z)$ , where $(F|_w g)(z) = (cz+d)^{-w} F(gz)$ . Then $F$ is identically zero.

In other words, a cusp form of nonpositive weight for a finite-index subgroup of $\mathrm{SL}_2(\mathbb Z)$ vanishes. For $w < 0$ the conclusion holds for every modular form (the cusp condition is then automatic up to a constant factor), while for $w = 0$ the cusp condition excludes the nonzero constants. The classical argument is the maximum-modulus principle: for weight $0$ , $|F|$ attains its supremum on finitely many truncated fundamental domains, so $F$ is constant and hence $0$ ; for $w < 0$ one applies the weight- $0$ case to $F^{12}\Delta^{-w}$ , using that the discriminant form $\Delta$ has no zeros on $\mathfrak H$ .

Formalization note. MDiff F is holomorphy on the upper half-plane, F ∣[w] γ is Mathlib's weight- $w$ slash action of $\gamma \in \mathrm{SL}_2(\mathbb Z)$ , so hinv is the weight- $w$ transformation law and hcusp is vanishing at all cusps (IsZeroAtImInfty of every $\mathrm{SL}_2(\mathbb Z)$ -translate). The statement extends Mathlib's level-one results ModularFormClass.levelOne_neg_weight_eq_zero and levelOne_weight_zero_const to arbitrary finite-index subgroups. It is the analytic input for the maximum-modulus step in the proof of MTT.period_vanishing (the Eichler integral of a cusp form with vanishing periods is a holomorphic form of weight $2-k \le 0$ vanishing at the cusps).

Preamble

import Mathlib.NumberTheory.ModularForms.Bounds
set_option autoImplicit false
noncomputable section
open UpperHalfPlane
open scoped ModularForm MatrixGroups Manifold

Formal statement

theorem MTT.eq_zero_of_slash_invariant_of_weight_nonpos
    {Γ : Subgroup SL(2, ℤ)} [Γ.FiniteIndex] {w : ℤ} (hw : w ≤ 0) {F : ℍ → ℂ}
    (hF : MDiff F) (hinv : ∀ γ ∈ Γ, F ∣[w] γ = F)
    (hcusp : ∀ g : SL(2, ℤ), IsZeroAtImInfty (F ∣[w] g)) : F = 0 := by sorry

Source

J. S. Milne, Modular Functions and Modular Forms (course notes, v1.31), Chapter 4, Theorem 4.9 and the remark closing its proof, p. 47: for a subgroup of finite index, modular forms of weight 0 are constant and there are no nonzero modular forms of negative weight (Milne's weight 2k); https://www.jmilne.org/math/CourseNotes/MF110.pdf. Level-one maximum-modulus proof: J.-P. Serre, A Course in Arithmetic, Chapter VII, §3.2, Theorem 4. Mathlib analogue at level one: ModularFormClass.levelOne_neg_weight_eq_zero, ModularFormClass.levelOne_weight_zero_const (Mathlib/NumberTheory/ModularForms/LevelOne/Basic.lean).

View graph

Cusp forms of nonpositive weight for a finite-index subgroup of SL2(Z)\mathrm{SL}_2(\mathbb Z)SL2​(Z) vanish

Cusp forms of nonpositive weight for a finite-index subgroup of $\mathrm{SL}_2(\mathbb Z)$ vanish