The q-expansion of a rational diagonal slash

The coprime-prime Hecke operator has, besides its upper-triangular sum, a term obtained by slashing by the rational matrix diag(d, 1). The same real matrix already defines the level-raising degeneracy map V_d; this file identifies the two constructions and transfers the existing q ↦ q ^ d formula for V_d to the rational slash action.

With the arithmetic normalization of the slash action, the unnormalised diagonal term is

f ∣[k] diag(d, 1) = d ^ (k - 1) V_d f.

Consequently its n-th Fourier coefficient is d ^ (k - 1) a_(n / d) when d ∣ n, and zero otherwise. This is the second term in the roadmap's recurrence a_n(T_p f) = a_(p n)(f) + χ(p) p ^ (k - 1) a_(n / p)(f); the factor χ(p) comes separately from the diamond operator and is not part of the diagonal slash.

Main results

• TauCeti.map_natDiagGL_d_one_eq_scaleGL: the rational diagonal representative maps to the real scaling matrix used by V_d.
• TauCeti.slash_natDiagGL_d_one_eq_smul_levelRaise: the rational diagonal slash is d ^ (k - 1) times the degeneracy map.
• ModularForm.qExpansion_slash_natDiagGL_d_one: the resulting power-series identity.
• The corresponding _coeff lemmas give the divisibility-conditional coefficient formula.

Provenance

The pointwise prime case corresponds to the private theorem slash_T_p_lower_eval in the AINTLIB LeanModularForms project (LeanModularForms/Modularforms/QExpansionSlash.lean, commit 112d12d95, Apache-2.0, LeanModularForms contributors). No code is transcribed: the result here is stated for every positive d and proved by identifying the rational matrix with Tau Ceti's existing scaleGL, after which the degeneracy-map and q-expansion APIs supply the formula without repeating AINTLIB's direct analytic argument.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.2--5.3.

@[simp]

theorem TauCeti.map_natDiagGL_d_one_eq_scaleGL {d : ℕ} [NeZero d] : (Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (HeckeRing.GLn.natDiagGL 2 ![d, 1]) = scaleGL d

The positive rational diagonal matrix diag(d, 1) maps to the real scaling matrix used to define the degeneracy operator V_d.

@[simp]

theorem TauCeti.slash_natDiagGL_d_one_apply {d : ℕ} [NeZero d] (k : ℤ) (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![d, 1]) f τ = ↑d ^ (k - 1) * f (scaleGL d • τ)

Slashing by the rational matrix diag(d, 1) is the same as slashing by scaleGL d, its real image. In particular it rescales the argument by d and contributes the arithmetic normalizing factor d ^ (k - 1).

theorem TauCeti.slash_natDiagGL_d_one_eq_smul_levelRaise {k : ℤ} {d : ℕ} {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} [𝒢'.HasDetOne] [NeZero d] (hle : 𝒢' ≤ ConjAct.toConjAct (scaleGL d)⁻¹ • 𝒢) (f : ModularForm 𝒢 k) : SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![d, 1]) ⇑f = ↑d ^ (k - 1) • ⇑(ModularForm.levelRaise d hle f)

The rational diagonal slash is a scaled degeneracy map. The target group hypothesis is exactly the one needed to package τ ↦ f (dτ) as V_d f; the equality itself is pointwise and contains no group-theoretic argument.

theorem ModularForm.qExpansion_slash_natDiagGL_d_one {k : ℤ} {d : ℕ} {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} [𝒢'.HasDetOne] [NeZero d] (h𝒢 : 1 ∈ 𝒢.strictPeriods) (h𝒢' : 1 ∈ 𝒢'.strictPeriods) (hle : 𝒢' ≤ ConjAct.toConjAct (TauCeti.scaleGL d)⁻¹ • 𝒢) (f : ModularForm 𝒢 k) : UpperHalfPlane.qExpansion 1 (SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![d, 1]) ⇑f) = ↑d ^ (k - 1) • (PowerSeries.expand d ⋯) (UpperHalfPlane.qExpansion 1 ⇑f)

The q-expansion of the rational diagonal slash. Slashing by diag(d, 1) multiplies the level-raised expansion by d ^ (k - 1), so the result is d ^ (k - 1) • (qExpansion f).expand d.

theorem ModularForm.qExpansion_slash_natDiagGL_d_one_coeff {k : ℤ} {d : ℕ} {𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)} [𝒢'.HasDetOne] [NeZero d] (h𝒢 : 1 ∈ 𝒢.strictPeriods) (h𝒢' : 1 ∈ 𝒢'.strictPeriods) (hle : 𝒢' ≤ ConjAct.toConjAct (TauCeti.scaleGL d)⁻¹ • 𝒢) (f : ModularForm 𝒢 k) (n : ℕ) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 (SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![d, 1]) ⇑f)) = if d ∣ n then ↑d ^ (k - 1) * (PowerSeries.coeff (n / d)) (UpperHalfPlane.qExpansion 1 ⇑f) else 0

The coefficient form of qExpansion_slash_natDiagGL_d_one: the diagonal term contributes d ^ (k - 1) a_(n / d) on indices divisible by d, and zero elsewhere.

theorem ModularForm.qExpansion_slash_natDiagGL_d_one_coeff_Gamma1 {k : ℤ} (M d : ℕ) [NeZero d] (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) (n : ℕ) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 (SlashAction.map k (HeckeRing.GLn.natDiagGL 2 ![d, 1]) ⇑f)) = if d ∣ n then ↑d ^ (k - 1) * (PowerSeries.coeff (n / d)) (UpperHalfPlane.qExpansion 1 ⇑f) else 0

The diagonal-slash coefficient formula at Γ₁. The source form has level M, while Gamma1_map_le_conjAct_scaleGL packages its scaled translate at level dM; this specialization is the form needed by the coprime Hecke recurrence.