The rational slash action of a diagonal Hecke representative

This file treats the rational diagonal Hecke representatives natDiagGL 2 a, specifically the scalar ones, and records how the weight-k rational slash action sees them: diag(c, c) acts trivially on the upper half-plane, so it only contributes the automorphy factor, which is c ^ (k - 2).

Main results

• ModularForm.rat_slash_natDiagGL_const: a nonzero constant rational diagonal acts by c ^ (k - 2).

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.3.

@[simp]

theorem ModularForm.rat_slash_natDiagGL_const {c : ℕ} [NeZero c] (k : ℤ) (f : UpperHalfPlane → ℂ) : SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![c, c]) f = ↑c ^ (k - 2) • f

A nonzero constant natural diagonal acts through the rational weight-k slash by c ^ (k - 2).