Forced zeros at the elliptic points i and ρ

The matrix S fixes i and S * T fixes ρ, with automorphy factors i and ρ + 1 there. These are primitive fourth and sixth roots of unity, so the transformation law of a form of weight k at the fixed point reads f z = ζᵏ f z. Hence a form invariant under S vanishes at i unless 4 ∣ k, and one invariant under S * T vanishes at ρ unless 6 ∣ k.

Main results

• TauCeti.ModularForm.apply_I_eq_zero_of_not_dvd: a form of weight k for a group containing S vanishes at i unless 4 ∣ k.
• TauCeti.ModularForm.apply_ρ_eq_zero_of_not_dvd: a form of weight k for a group containing S * T vanishes at ρ unless 6 ∣ k.

References

• J.-P. Serre, A Course in Arithmetic, VII.3.

theorem TauCeti.ModularForm.apply_I_eq_zero_of_not_dvd {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [SlashInvariantFormClass F Γ k] (hS : (Matrix.SpecialLinearGroup.mapGL ℝ) ModularGroup.S ∈ Γ) (f : F) (hk : ¬4 ∣ k) : f UpperHalfPlane.I = 0

A form of weight k for a group containing S vanishes at the elliptic point i unless 4 ∣ k.

theorem TauCeti.ModularForm.apply_ρ_eq_zero_of_not_dvd {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [SlashInvariantFormClass F Γ k] (hST : (Matrix.SpecialLinearGroup.mapGL ℝ) (ModularGroup.S * ModularGroup.T) ∈ Γ) (f : F) (hk : ¬6 ∣ k) : f UpperHalfPlane.ρ = 0

A form of weight k for a group containing S * T vanishes at the elliptic point ρ unless 6 ∣ k.