Uniqueness from positive Fourier coefficients

At nonzero weight, a modular form whose group has finite-index intersection with the modular group is determined by its positive Fourier coefficients. The omitted constant term cannot hide a nonzero constant modular form: a finite-index intersection with the modular group contains a lower unipotent matrix, whose automorphy factor is nonconstant.

This allows coefficient identities at positive indices to imply identities of modular forms, without imposing a spurious condition on the constant term of an Eisenstein series.

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, Proposition 5.8.5.

theorem TauCeti.ModularForm.eq_zero_of_forall_pos_qExpansion_coeff_eq_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (hk : k ≠ 0) {f : ModularForm Γ k} (hf : ∀ (n : ℕ), 0 < n → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = 0) : f = 0

At nonzero weight, vanishing of all positive Fourier coefficients forces a modular form whose group has finite-index intersection with the modular group to vanish.

theorem TauCeti.ModularForm.eq_of_forall_pos_qExpansion_coeff_eq {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (hk : k ≠ 0) {f g : ModularForm Γ k} (hfg : ∀ (n : ℕ), 0 < n → (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑g)) : f = g

At nonzero weight, equality of the positive Fourier coefficients determines a modular form. The constant coefficient need not be supplied.

theorem TauCeti.ModularForm.weight_ne_zero_of_pos_qExpansion_coeff_ne_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [Γ.IsFiniteRelIndex (Matrix.SpecialLinearGroup.mapGL ℝ).range] {h : ℝ} (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {f : ModularForm Γ k} {n : ℕ} (hn : 0 < n) (hc : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) ≠ 0) : k ≠ 0

A nonzero positive Fourier coefficient excludes weight zero when the group has finite-index intersection with the modular group.