The descent slash sum does not see the level away from p

The descent family descendMatrix p N at a prime p ∣ N consists of the p upper-triangular matrices [1, v; 0, p], which do not depend on N at all, together with — exactly when p² ∤ N — one extra representative [1, 0; 0, p] · γ_N, where γ_N ∈ SL(2, ℤ) is chosen congruent to S modulo p and to 1 modulo N / p. Replacing N by l N with l coprime to p leaves the count unchanged and replaces γ_N by some γ_{lN}, which satisfies the same two congruences; so γ_{lN} γ_N⁻¹ is congruent to 1 modulo p and modulo N / p, hence modulo N, and conjugating it through [1, 0; 0, p] produces an element of Γ₁(N) (exists_mem_Gamma1_descendMatrix_mul_left_eq). A function invariant under Γ₁(N) therefore has the same descent slash sum at the two levels (descendSlash_mul_left_of_coprime): Miyake's Lemma 4.6.6, in the form the level-lowering induction consumes.

Main results

• TauCeti.descendMatrixCount_mul_left_of_coprime: the size of the descent family at l N equals its size at N when l is coprime to p.
• TauCeti.exists_mem_Gamma1_descendMatrix_mul_left_eq: the extra representatives at levels l N and N differ on the left by an element of Γ₁(N).
• TauCeti.descendSlash_mul_left_of_coprime: the descent slash sum is the same at levels l N and N for every function invariant under Γ₁(N).

Provenance

descendCosetList_slash_sum_rep_invariance and descendCosetList_slash_sum_commute of the AINTLIB LeanModularForms project (StrongMultiplicityOne/LevelCommute.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), which assume a nebentypus; here the invariance is derived from Γ₁(N) alone, since the two extra representatives differ by an element of Γ(N) conjugated into Γ₁(N).

References

• T. Miyake, Modular forms, Lemma 4.6.6.

theorem TauCeti.descendMatrixCount_mul_left_of_coprime {p l : ℕ} (hpl : p.Coprime l) (N : ℕ) : descendMatrixCount p (l * N) = descendMatrixCount p N

The descent family has the same size at l N as at N when l is coprime to p.

theorem TauCeti.exists_mem_Gamma1_descendMatrix_mul_left_eq {p l N : ℕ} (hp : Nat.Prime p) (hpN : p ∣ N) (hpl : p.Coprime l) {v : Fin (descendMatrixCount p N)} (hv : p ≤ ↑v) {w : Fin (descendMatrixCount p (l * N))} (hw : p ≤ ↑w) : ∃ ε ∈ CongruenceSubgroup.Gamma1 N, descendMatrix p (l * N) w = (Matrix.SpecialLinearGroup.mapGL ℝ) ε * descendMatrix p N v

The extra representatives at levels l N and N differ on the left by Γ₁(N).

theorem TauCeti.descendSlash_mul_left_of_coprime {p l N : ℕ} (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) (hpl : p.Coprime l) {f : UpperHalfPlane → ℂ} (hf : ∀ ε ∈ CongruenceSubgroup.Gamma1 N, SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ε) f = f) : descendSlash k p (l * N) f = descendSlash k p N f

Miyake, Lemma 4.6.6 — the descent slash sum does not see the level away from p. For l coprime to p and f invariant under Γ₁(N), the descent slash sums of f at levels l N and N coincide.