The double coset of diag(1, p) is stable under conjugation by Γ₀(N)

The diamond operators act on M_k(Γ₁(N)) through Γ₀(N) ⧸ Γ₁(N), and they commute with Tₚ. On the Hecke-ring side that commutation is not an analytic fact but a statement about double cosets. The diamond ⟨d⟩ is the basis element of Γ₁(N) · g · Γ₁(N) for a g ∈ Γ₀(N), and such a g normalizes Γ₁(N), so products taken with it carry no structure constant (HeckeCosetModule.single_mul_single_of_mem_normalizer, and single_diamondCosetGamma1_mul_single_diamondCosetGamma1 for the diamonds among themselves). Commuting ⟨d⟩ past the basis element of Γ₁(N) · diag(1, p) · Γ₁(N) therefore comes down to one equation between double cosets,

Γ₁(N) · (g · diag(1, p)) · Γ₁(N) = Γ₁(N) · (diag(1, p) · g) · Γ₁(N),

which — g normalizing Γ₁(N), so that a Γ₁(N) factor may be moved across it — is exactly the assertion that conjugating diag(1, p) by g does not leave the double coset. This file proves that assertion, for p prime.

The two branches, and why neither covers the other

Write g = !![a, b; c, e] ∈ Γ₀(N), so N ∣ c and a e − b c = 1. The conjugate is

g · diag(1, p) · g⁻¹ = !![1 + b c (1 − p), a b (p − 1); c e (1 − p), p + b c (p − 1)],

and membership in the double coset means writing it as τ · diag(1, p) · γ with τ, γ ∈ Γ₁(N).

• e coprime to p. The right factor can be taken to be a power of T = !![1, 1; 0, 1]: the congruence p ∣ b + j e is solvable because e is invertible modulo p, and then τ = C · (diag(1, p) · Tʲ)⁻¹ is integral of determinant one and satisfies the Γ₁(N) congruences, because N ∣ c makes the whole lower row divisible by N.
• p ∣ e. No power of T can work, so this is not a gap in the first argument: p ∣ e together with a e − b c = 1 forces b c ≡ −1 (mod p), hence p ∤ b once 1 < p, while p ∣ b + j e reduces to p ∣ b. What happens instead is that the conjugate's first column becomes divisible by p — writing e = p f, the (0, 0) entry is a e − b c p = p (a f − b c) — so the conjugate factors as τ′ · diag(1, p) · γ with γ = !![a f p, b c′; N, 1] ∈ Γ₁(N), writing c = N c′. The product diag(1, p) · γ is then the twisted representative σ · diag(p, 1) rather than an upper-triangular one.

The coprime branch reads its offset straight off a Bézout pair for e and p, and both outer factors land in Γ₁(N) — the left one because N ∣ c makes the whole lower row divisible by N, the right one because every power of T lies in Γ₁(N).

At a prime the two branches are exhaustive, which is conj_natDiagGL_mem_doubleCoset_of_prime. Neither needs p to be prime on its own, and neither needs a coprimality hypothesis relating p to N: reducing a (p f) − b c = 1 along N ∣ c leaves (a f) p ≡ 1 (mod N), so p is automatically invertible modulo the level wherever the twisted branch needs it.

Main results

• HeckeRing.GL2.conj_natDiagGL_mem_doubleCoset_of_isCoprime: the coprime branch.
• HeckeRing.GL2.conj_natDiagGL_mem_doubleCoset_of_dvd: the branch where p divides the lower-right entry of the conjugating matrix.
• HeckeRing.GL2.conj_natDiagGL_mem_doubleCoset_of_prime: the two combined, at a prime.

Provenance

No code is transcribed, and the statement has no counterpart to port. The AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0, commit 6d87d596a5372d5b122c47b7082d4c3afa9b7c3b) proves the diamond/Hecke commutation twice, but never on the coset side: HeckeRing.GL2.heckeT_n_comm_diamondOp (HeckeRIngs/GL2/Unified/RingTransport.lean:298) argues on the character eigenspace, where the diamond is the scalar χ(d) and commutation is automatic, and heckeT_p_comm_diamondOp (HeckeRIngs/GL2/HeckeT_p.lean:983) is an operator-level slash identity. Both take the analytic action as given; the double-coset statement below is what a Hecke ring needs, and is proved here from the group law and the matrix entries.

References

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

theorem HeckeRing.GL2.conj_natDiagGL_mem_doubleCoset_of_isCoprime {N p : ℕ} (hp : 0 < p) {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hg : g ∈ CongruenceSubgroup.Gamma0 N) (hco : IsCoprime (↑g 1 1) ↑p) : (Matrix.SpecialLinearGroup.mapGL ℚ) g * GLn.natDiagGL 2 ![1, p] * (Matrix.SpecialLinearGroup.mapGL ℚ) g⁻¹ ∈ DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, p]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N))

Conjugation by Γ₀(N) fixes the double coset of diag(1, p), when the lower-right entry of the conjugating matrix is coprime to p. The complementary case, where p divides that entry, is conj_natDiagGL_mem_doubleCoset_of_dvd.

theorem HeckeRing.GL2.conj_natDiagGL_mem_doubleCoset_of_dvd {N p : ℕ} (hp : 0 < p) {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hg : g ∈ CongruenceSubgroup.Gamma0 N) (he : ↑p ∣ ↑g 1 1) : (Matrix.SpecialLinearGroup.mapGL ℚ) g * GLn.natDiagGL 2 ![1, p] * (Matrix.SpecialLinearGroup.mapGL ℚ) g⁻¹ ∈ DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, p]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N))

Conjugation by Γ₀(N) fixes the double coset of diag(1, p), when p divides the lower-right entry of the conjugating matrix. The complementary case, where that entry is coprime to p, is conj_natDiagGL_mem_doubleCoset_of_isCoprime.

theorem HeckeRing.GL2.conj_natDiagGL_mem_doubleCoset_of_prime {N p : ℕ} (hp : Nat.Prime p) {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hg : g ∈ CongruenceSubgroup.Gamma0 N) : (Matrix.SpecialLinearGroup.mapGL ℚ) g * GLn.natDiagGL 2 ![1, p] * (Matrix.SpecialLinearGroup.mapGL ℚ) g⁻¹ ∈ DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, p]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N))

The Γ₁(N) double coset of diag(1, p) is stable under conjugation by Γ₀(N), for p prime.

Combines conj_natDiagGL_mem_doubleCoset_of_dvd and conj_natDiagGL_mem_doubleCoset_of_isCoprime, which between them cover every case at a prime.