Tₚ and the degeneracy operator V_d

The degeneracy operator V_d : S_k(Γ₁(M)) → S_k(Γ₁(N)), (V_d f) τ = f (d τ), raises the level along d * M ∣ N. This file proves that it commutes with the Hecke operator Tₚ at every prime p coprime to N, and computes Tₚ (V_d f) at the primes dividing N. These are the inputs to the statement that Tₚ preserves the old subspace at every prime, and to the stability of the new subspace at primes coprime to N.

The shape of the proof at primes coprime to the level

Tₚ at a prime is heckeSlashUpperTri k p f + (⟨p⟩ f) ∣[k] diag(p, 1), and V_d is — up to the normalising scalar d ^ (k - 1) — the slash by diag(d, 1). So the theorem splits into a statement about each summand, and each is proved in the diag(d, 1)-slash form, where the normalising scalars are absent:

• the upper-triangular sum, which commutes by heckeSlashUpperTri_slash_scaleRep_comm (HeckeSlash/UpperTri/Periodic.lean): the two slashes do not commute termwise, but the part of d b that leaves the range b < p becomes a shift T ^ q, which invariance under T absorbs, and coprimality of d and p makes the surviving index a permutation of Fin p. The Γ₁(M)-invariance of f supplies that hypothesis, through slash_mapGL_T.
• the diamond term, which commutes because natural diagonal matrices do — HeckeRing.GLn.natDiagGL_comm — once TauCeti.CuspForm.diamondOpCusp_levelRaise has moved ⟨p⟩ across V_d.

Main results

• HeckeRing.GL2.heckeTCuspNat_levelRaise: Tₚ (V_d f) = V_d (Tₚ f) for p prime and coprime to the raised level N.
• HeckeRing.GL2.heckeTCuspNat_levelRaise_mul: T_n (V_{n e} f) = V_e f whenever n * e * M ∣ N; at a prime this is Uₚ V_p = 1.
• HeckeRing.GL2.heckeTCuspNat_levelRaise_of_primeFactors_subset: T_n (V_d f) = V_d (T_n f) when every prime factor of n divides M and n is coprime to d.
• HeckeRing.GL2.heckeTCuspNat_levelRaise_eq_sub: Tₚ (V_d f) = V_d (Tₚ f) - p ^ (k - 1) • V_{d p} (⟨p⟩ f) for a prime p coprime to d with d * p * M ∣ N.

The primes dividing the level

At an index n all of whose prime factors divide N, the operator T_n on S_k(Γ₁(N)) reads off the coefficients a_{n m} (qExpansion_coeff_heckeTCuspNat_of_primeFactors_subset), and aₘ(V_d f) = a_{m/d}(f) when d ∣ m and 0 otherwise. The three formulas above are identities of q-expansions, turned into identities of cusp forms by CuspForm.qExpansion_injective. In the last one the diamond term of the level-M recurrence aₘ(Tₚ f) = a_{p m}(f) + p ^ (k - 1) a_{m/p}(⟨p⟩ f) there is what the correction V_{d p} (⟨p⟩ f) removes.

Provenance

The mathematics follows heckeT_p_all_levelRaise_comm and its supporting lemmas in the AINTLIB LeanModularForms project, file LeanModularForms/HeckeRIngs/GL2/Newforms/LevelRaiseComm.lean, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck, lines 45–311. No proof code is transcribed: that development works with bare coset functions heckeT_p_ut and heckeT_p_fun and a Γ₁-shift matrix of its own, and splits Tₚ on whether p divides the level, whereas here Tₚ is the single-formula operator of HeckeSlash/Operators.lean, the shift is Mathlib's ModularGroup.T, and the level-raise is the general TauCeti.CuspForm.levelRaise of ModularForms/Degeneracy.lean, stated at d * M ∣ N rather than at d * M = N. The reindexing half of that argument (source lines 66–190) lives with the upper-triangular sum in HeckeSlash/UpperTri/Periodic.lean, which carries its own note.

References

• F. Diamond and J. Shurman, A first course in modular forms, Proposition 5.6.2.

The shift matrix

Tₚ and V_d

theorem HeckeRing.GL2.heckeTCuspNat_levelRaise {M d N p : ℕ} (k : ℤ) (hdvd : d * M ∣ N) (hp : Nat.Prime p) (hpN : p.Coprime N) (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (heckeTCuspNat k p) (TauCeti.CuspForm.levelRaise d ⋯ f) = TauCeti.CuspForm.levelRaise d ⋯ ((heckeTCuspNat k p) f)

Tₚ commutes with the degeneracy operator V_d. For d * M ∣ N and a prime p coprime to N, raising the level of f and then applying Tₚ at level N agrees with applying Tₚ at level M and then raising the level.

Coprimality is not decoration: at p ∣ N the diamond term of Tₚ vanishes at level N but need not vanish at level M, and b ↦ d b mod p stops being a permutation once p ∣ d.

T_n and V_d at indices supported on the level

theorem HeckeRing.GL2.heckeTCuspNat_levelRaise_mul {M N : ℕ} (k : ℤ) {n e : ℕ} [NeZero N] (hdvd : n * e * M ∣ N) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (heckeTCuspNat k n) (TauCeti.CuspForm.levelRaise (n * e) ⋯ g) = TauCeti.CuspForm.levelRaise e ⋯ g

T_n undoes the degeneracy operator V_n: for n * e * M ∣ N, T_n (V_{n e} g) = V_e g at level N. Every prime factor of n divides N, so T_n reads off the coefficients a_{n m}, and those of V_{n e} g are the coefficients of V_e g. At e = 1 this is the classical U_p V_p = 1.

theorem HeckeRing.GL2.heckeTCuspNat_levelRaise_of_primeFactors_subset {M d N : ℕ} (k : ℤ) {n : ℕ} [NeZero N] [NeZero n] (hdvd : d * M ∣ N) (hn : n.primeFactors ⊆ M.primeFactors) (hnd : n.Coprime d) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (heckeTCuspNat k n) (TauCeti.CuspForm.levelRaise d ⋯ g) = TauCeti.CuspForm.levelRaise d ⋯ ((heckeTCuspNat k n) g)

T_n commutes with V_d when n is supported on the source level and prime to d: for d * M ∣ N, n coprime to d and every prime factor of n dividing M, T_n (V_d g) = V_d (T_n g). At both levels T_n reads off the coefficients a_{n m}, and coprimality makes d ∣ n m equivalent to d ∣ m.

This is the bad-index counterpart of heckeTCuspNat_levelRaise.

theorem HeckeRing.GL2.heckeTCuspNat_levelRaise_eq_sub {M d N p : ℕ} (k : ℤ) [NeZero N] (hp : Nat.Prime p) (hpd : p.Coprime d) (hdvd : d * p * M ∣ N) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k) : (heckeTCuspNat k p) (TauCeti.CuspForm.levelRaise d ⋯ g) = TauCeti.CuspForm.levelRaise d ⋯ ((heckeTCuspNat k p) g) - ↑p ^ (k - 1) • TauCeti.CuspForm.levelRaise (d * p) ⋯ ((diamondOpCuspNat k p) g)

Tₚ on V_d g at a prime dividing the level but not d: for p prime to d with d * p * M ∣ N, Tₚ (V_d g) = V_d (Tₚ g) - p ^ (k - 1) • V_{d p} (⟨p⟩ g). At level N the operator Tₚ is Uₚ, reading off a_{p m}; at level M the diamond term of the recurrence for Tₚ is exactly what the degeneracy image V_{d p} (⟨p⟩ g) cancels. When p ∣ M that diamond term is 0, and this reduces to heckeTCuspNat_levelRaise_of_primeFactors_subset.