The upper-triangular Hecke slash sum under T-invariance

The classical upper-triangular Hecke sum heckeSlashUpperTri k p f = ∑ b < p, f ∣[k] !![1, b; 0, p] preserves invariance under the translation matrix T = !![1, 1; 0, 1].

Right multiplication of the representative !![1, b; 0, p] by T produces !![1, b + 1; 0, p]. For b < p - 1, this is the (b + 1)-st representative; for b = p - 1, it factors as T · !![1, 0; 0, p]. When f is T-slash invariant (f ∣[k] T = f), the T factor on the boundary term is absorbed, so slashing the whole sum by T cyclically permutes the summands via finRotate p and recovers heckeSlashUpperTri k p f.

Pointwise on ℍ, f ∣[k] T = f is the 1-periodicity f(τ + 1) = f(τ), so the upper-triangular sum sends 1-periodic functions to 1-periodic functions.

The same absorption proves a second statement about a T-invariant f: the sum commutes with the slash by scaleRep d = diag(d, 1) for d coprime to p. The two slashes do not commute termwise — diag(d, 1) · !![1, b; 0, p] is !![1, d b; 0, p] · diag(d, 1), whose upper entry d b leaves the range b < p — but writing d b = q p + r puts the excess into a shift T ^ q, which the invariance absorbs, and coprimality makes b ↦ r a permutation of Fin p, so the sum is merely reindexed. This is the level-raising half of Tₚ ∘ V_d = V_d ∘ Tₚ (HeckeSlash/Degeneracy.lean).

Main results

• HeckeRing.GL2.upperTriRep_mul_mapGL_T_of_lt: for b.val + 1 < p, upperTriRep p b * mapGL ℚ ModularGroup.T = upperTriRep p ⟨b.val + 1, _⟩.
• HeckeRing.GL2.upperTriRep_last_mul_mapGL_T: for b.val + 1 = p, upperTriRep p b * mapGL ℚ ModularGroup.T = mapGL ℚ ModularGroup.T * upperTriRep p ⟨0, _⟩.
• HeckeRing.GL2.heckeSlashUpperTri_slash_T: if f ∣[k] mapGL ℚ ModularGroup.T = f, then heckeSlashUpperTri k p f ∣[k] mapGL ℚ ModularGroup.T = heckeSlashUpperTri k p f.
• HeckeRing.GL2.heckeSlashUpperTri_shift_one: if f((1 : ℝ) +ᵥ τ) = f(τ) for all τ, then heckeSlashUpperTri k p f ((1 : ℝ) +ᵥ τ) = heckeSlashUpperTri k p f τ.
• HeckeRing.GL2.heckeSlashUpperTri_slash_scaleRep_comm: if f ∣[k] mapGL ℚ ModularGroup.T = f and d is coprime to p, then heckeSlashUpperTri k p (f ∣[k] scaleRep d) equals heckeSlashUpperTri k p f ∣[k] scaleRep d.

Provenance

heckeSlashUpperTri_slash_scaleRep_comm and its helpers adapt the reindexing step of the level-raising comparison in the AINTLIB LeanModularForms project, file LeanModularForms/HeckeRIngs/GL2/Newforms/LevelRaiseComm.lean, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck, lines 66–190 (T_p_upper_mod, levelRaise_mul_T_p_upper and sum_reindex_mul_mod, feeding heckeT_p_ut_levelRaise). No proof code is transcribed: that development sums over Finset.range p by Finset.sum_nbij and assumes p prime, whereas the statement here indexes by Fin p through an explicit Equiv, assumes only 0 < p with Nat.Coprime d p, and is about a bare function rather than a cusp form. Its consumer, and the provenance note for the level-raising theorem itself, is HeckeSlash/Degeneracy.lean.

References

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

theorem HeckeRing.GL2.upperTriRep_mul_mapGL_T_of_lt (p : ℕ) (b : Fin p) (hb : ↑b + 1 < p) : upperTriRep p b * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T = upperTriRep p ⟨↑b + 1, hb⟩

For b.val + 1 < p, right multiplication of upperTriRep p b by T shifts the offset to b + 1.

theorem HeckeRing.GL2.upperTriRep_last_mul_mapGL_T (p : ℕ) (b : Fin p) (hb : ↑b + 1 = p) : upperTriRep p b * (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T = (Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T * upperTriRep p ⟨0, ⋯⟩

For the last representative b.val + 1 = p, right multiplication by T factors as T · upperTriRep p 0.

theorem HeckeRing.GL2.heckeSlashUpperTri_slash_T (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ) (hfT : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T) f = f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T) (heckeSlashUpperTri k p f) = heckeSlashUpperTri k p f

The upper-triangular Hecke slash sum preserves T-invariance.

theorem HeckeRing.GL2.heckeSlashUpperTri_shift_one (k : ℤ) (p : ℕ) (f : UpperHalfPlane → ℂ) (hf : ∀ (τ : UpperHalfPlane), f (1 +ᵥ τ) = f τ) (τ : UpperHalfPlane) : heckeSlashUpperTri k p f (1 +ᵥ τ) = heckeSlashUpperTri k p f τ

Pointwise 1-periodicity: heckeSlashUpperTri preserves translation invariance f((1 : ℝ) +ᵥ τ) = f(τ).

The sum against diag(d, 1)

theorem HeckeRing.GL2.scaleRep_mul_upperTriRep (p : ℕ) {d : ℕ} (hd : 0 < d) (b : Fin p) {q r : ℕ} (hr : r < p) (hqr : d * ↑b = q * p + r) : scaleRep d * upperTriRep p b = (Matrix.SpecialLinearGroup.mapGL ℚ) (ModularGroup.T ^ q) * (upperTriRep p ⟨r, hr⟩ * scaleRep d)

The commutation of scaleRep d = diag(d, 1) past an upper-triangular representative. Both sides are !![d, d b; 0, p]: on the right, d b = q p + r is split so that the representative index r is again in range, at the cost of the shift T ^ q.

theorem HeckeRing.GL2.heckeSlashUpperTri_slash_scaleRep_comm (k : ℤ) (p : ℕ) {d : ℕ} (hd : 0 < d) (hp : 0 < p) (hdp : d.Coprime p) {f : UpperHalfPlane → ℂ} (hT : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℚ) ModularGroup.T) f = f) : heckeSlashUpperTri k p (SlashAction.map k (scaleRep d) f) = SlashAction.map k (scaleRep d) (heckeSlashUpperTri k p f)

The upper-triangular slash sum commutes with the slash by scaleRep d = diag(d, 1), for d coprime to p and any T-invariant function. This is the level-raising half of heckeTCuspNat_levelRaise, stated before the normalising scalar of V_d is introduced.

Invariance under T alone is all the reindexing consumes: the shift it produces is T ^ q for the quotient q of d b by p, and those powers are derived from hT inside the proof, so no level and no explicit power enters the statement. A form invariant under a congruence subgroup containing T — every Γ₁(M) — meets the hypothesis; HeckeSlash/Degeneracy.lean is the consumer.