The q-expansion of the upper-triangular Hecke sum

UpperTri/Sum.lean defines heckeSlashUpperTri k p f = ∑ b < p, f ∣[k] !![1, b; 0, p], and the files beside it carry it past holomorphy, the cusps and invariance under T. What was missing is what the sum does to Fourier coefficients, and that is what this file computes:

aₘ(heckeSlashUpperTri k p f) = a_{p m}(f).

Three steps do it. Slashing by !![1, b; 0, p] sends τ to (τ + b) / p, and both the determinant and the denominator are p, so the automorphy factor is p ^ (k - 1) * p ^ (-k), that is p⁻¹: the weight cancels out, which is why the answer below carries no power of p. The local parameter then splits, 𝕢 1 ((τ + b) / p) = 𝕢 p τ * 𝕢 p b. Finally the offsets contribute the p-th roots of unity 𝕢 p b, whose m-th powers sum to p exactly when p ∣ m (TauCeti.Periodic.sum_qParam_natCast_pow); the p cancels the p⁻¹, and only the indices in p ℕ survive.

Two conventions worth stating

• This is the operator that Diamond–Shurman's Tₚ degenerates to at p ∣ N — the one modern papers write Uₚ. Following the sources, no separate Uₚ is introduced: the classical Tₚ will be built on top of this sum, and at p ∣ N it is this sum. For p ∤ N the classical Tₚ has one further coset representative, !![p, 0; 0, 1], which contributes the second term χ(p) p ^ (k - 1) a_{m/p}(f) of the recurrence; that representative is not part of this sum and does not appear here.
• The expansions are taken at width 1, which is the width of ∞ for every group between Γ₁(N) and Γ₀(N). The hypotheses are the three that Mathlib's q-expansion API asks of a raw function on ℍ — periodicity through ofComplex, holomorphy, boundedness at i∞ — and qExpansion_coeff_heckeSlashUpperTri' discharges all three from ModularFormClass.

Main results

• HeckeRing.GL2.coe_upperTriRep_smul, HeckeRing.GL2.qParam_one_upperTriRep_smul: the Möbius image (τ + b) / p of a representative, and the resulting factorisation of the local parameter.
• HeckeRing.GL2.slash_upperTriRep_apply: slashing by a representative is p⁻¹ * f ((τ + b)/p), whatever the weight.
• HeckeRing.GL2.hasSum_qExpansion_heckeSlashUpperTri: the sum is given everywhere by the convergent expansion ∑ j, a_{p j}(f) q ^ j.
• HeckeRing.GL2.qExpansion_coeff_heckeSlashUpperTri and qExpansion_heckeSlashUpperTri: the coefficient formula aₘ = a_{p m} and its power-series form, and qExpansion_coeff_heckeSlashUpperTri', the same for a bundled modular form.
• HeckeRing.GL2.periodic_heckeSlashUpperTri: the periodicity fact used by the coefficient uniqueness argument.

Provenance

No code is transcribed. The computation is the classical one — the q-expansion of the operator Diamond–Shurman write Tₚ — run here through Mathlib's q-expansion API and the roots-of-unity orthogonality relation, rather than through a transcribed proof.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.2–5.3.
• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.5.

theorem HeckeRing.GL2.coe_upperTriRep_smul (p : ℕ) (b : Fin p) (τ : UpperHalfPlane) : ↑((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (upperTriRep p b) • τ) = (↑τ + ↑↑b) / ↑p

The Möbius image of τ under !![1, b; 0, p] is (τ + b) / p.

theorem HeckeRing.GL2.qParam_one_upperTriRep_smul (p : ℕ) (b : Fin p) (τ : UpperHalfPlane) : Function.Periodic.qParam 1 ↑((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (upperTriRep p b) • τ) = Function.Periodic.qParam ↑p ↑τ * Function.Periodic.qParam ↑p ↑↑b

The local parameter of width 1 at (τ + b) / p factors as the parameter of width p at τ times its value at the offset b.

theorem HeckeRing.GL2.slash_upperTriRep_apply (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ) (b : Fin p) (τ : UpperHalfPlane) : SlashAction.map k (upperTriRep p b) f τ = (↑p)⁻¹ * f ((Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)) (upperTriRep p b) • τ)

Slashing by !![1, b; 0, p]: the determinant and the denominator are both p, so the automorphy factor collapses to p ^ (k - 1) * p ^ (-k) = p⁻¹, independent of the weight.

theorem HeckeRing.GL2.hasSum_qExpansion_heckeSlashUpperTri (k : ℤ) (p : ℕ) (hp : 0 < p) {f : UpperHalfPlane → ℂ} (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (hfhol : MDiff f) (hfbdd : UpperHalfPlane.IsBoundedAtImInfty f) (τ : UpperHalfPlane) : HasSum (fun (j : ℕ) => (PowerSeries.coeff (p * j)) (UpperHalfPlane.qExpansion 1 f) • Function.Periodic.qParam 1 ↑τ ^ j) (heckeSlashUpperTri k p f τ)

The upper-triangular Hecke sum has the q-expansion of f along the progression p ℕ. Summing the twisted expansion of each representative over the offsets b < p, the roots-of-unity orthogonality relation kills every term whose index is not divisible by p, and the surviving terms are exactly a_{p j}(f) q^j.

theorem HeckeRing.GL2.periodic_heckeSlashUpperTri (k : ℤ) (p : ℕ) {f : UpperHalfPlane → ℂ} (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) : Function.Periodic (heckeSlashUpperTri k p f ∘ ↑UpperHalfPlane.ofComplex) 1

The upper-triangular sum of a 1-periodic function is 1-periodic, in the ofComplex-extended form the q-expansion API asks for.

@[simp]

theorem HeckeRing.GL2.qExpansion_coeff_heckeSlashUpperTri (k : ℤ) (p : ℕ) (hp : 0 < p) {f : UpperHalfPlane → ℂ} (hfper : ∀ (x : ℂ), f (↑UpperHalfPlane.ofComplex (x + 1)) = f (↑UpperHalfPlane.ofComplex x)) (hfhol : MDiff f) (hfbdd : UpperHalfPlane.IsBoundedAtImInfty f) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 (heckeSlashUpperTri k p f)) = (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 f)

The coefficient formula for the upper-triangular Hecke sum: aₘ(∑_{b < p} f ∣[k] !![1, b; 0, p]) = a_{p m}(f).

This is the operator classical sources write Uₚ at p ∣ N, and it is the first half of the Diamond–Shurman recurrence aₘ(Tₚ f) = a_{m p}(f) + χ(p) p^{k−1} a_{m/p}(f); the second term comes from the remaining representative !![p, 0; 0, 1], which is not part of this sum. Note that the weight has disappeared: the automorphy factor of each representative is p⁻¹ whatever k is, and the p cancels against the number of offsets.

theorem HeckeRing.GL2.qExpansion_heckeSlashUpperTri (k : ℤ) (p : ℕ) (hp : 0 < p) {f : UpperHalfPlane → ℂ} (hfper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) 1) (hfhol : MDiff f) (hfbdd : UpperHalfPlane.IsBoundedAtImInfty f) : UpperHalfPlane.qExpansion 1 (heckeSlashUpperTri k p f) = PowerSeries.mk fun (m : ℕ) => (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 f)

qExpansion_coeff_heckeSlashUpperTri as an identity of power series: the upper-triangular sum extracts the subseries of f supported on the multiples of p, reindexed.

@[simp]

theorem HeckeRing.GL2.qExpansion_coeff_heckeSlashUpperTri' (k : ℤ) (p : ℕ) {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} [ModularFormClass F Γ k] (hΓ : 1 ∈ Γ.strictPeriods) (hp : 0 < p) (f : F) (m : ℕ) : (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 (heckeSlashUpperTri k p ⇑f)) = (PowerSeries.coeff (p * m)) (UpperHalfPlane.qExpansion 1 ⇑f)

The coefficient formula for a bundled modular form, the shape Layer 2(b) consumes: for f a modular form of weight k on a group with 1 among its strict periods — every congruence subgroup between Γ₁(N) and Γ₀(N) has this, since it contains T — the upper-triangular sum reads off the coefficients of f along p ℕ.