Injectivity of the period map

For a finite-index subgroup Γ ≤ SL(2, ℤ), the periods of a cusp form of weight k = w + 2 determine the form. This holds for the period map with coefficients in any commutative ring R equipped with an algebra map to ℂ, in particular for the integral modular symbols.

If the period functional vanishes, all monomial periods vanish, including those of each translate of the form. The transformation law of the Eichler integral then identifies its weight--w slash at every cusp with the Eichler integral of the translated cusp form. Thus it vanishes at every cusp and is a modular form of nonpositive weight. Mathlib's negative-weight vanishing and weight-zero constancy force it to vanish. Differentiating w + 1 times recovers the original cusp form.

Together with Hecke equivariance, injectivity allows relations among integral operators on modular symbols to be transferred to operators on cusp forms.

Main results

• TauCeti.ModularSymbols.periodMap_injective: the period map is injective for k = w + 2.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §8.2.
• M. Eichler, Eine Verallgemeinerung der Abelschen Integrale, Math. Z. 67 (1957), 267–298.
• The AINTLIB LeanModularForms project, ModularSymbols/EichlerInjective.lean (periodMap'_injective_eichler), for the Eichler-integral route to injectivity. No code is transcribed; the proof uses the Eichler-integral and period APIs already in Tau Ceti.

theorem TauCeti.ModularSymbols.periodMap_injective {R : Type u_1} [CommRing R] [Algebra R ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex] {k : ℤ} {w : ℕ} (hk : k = ↑w + 2) : Function.Injective ⇑(periodMap R Γ hk)

Periods determine a cusp form. For a finite-index subgroup of SL(2, ℤ) and weight k = w + 2 ≥ 2, the period map into the dual of the modular symbols over R is injective. In particular this applies to the integral modular symbols (R = ℤ).