The Γ₀(N) double coset of a coprime-determinant element

Shimura, Lemma 3.29(3). For α ∈ Δ₀(N) whose determinant is coprime to N,

SL₂(ℤ) α SL₂(ℤ) ∩ Δ₀(N) = Γ₀(N) α Γ₀(N).

The right-hand side is always contained in the left, because Γ₀(N) ≤ SL₂(ℤ) and Δ₀(N) is a submonoid containing both Γ₀(N) and α. The content is the other inclusion: an element σ₁ α σ₂ of the level-one double coset that happens to lie in Δ₀(N) can be rewritten with σ₁, σ₂ taken from Γ₀(N).

The mechanism is the Chinese-remainder decomposition CongruenceSubgroup.Gamma_gcd_eq_sup: coprimality of det α with N makes Γ(N) ⊔ Γ(det α) = ⊤, so σ₁ factors as τ_N · τ_a with τ_N ∈ Γ(N) ≤ Γ₀(N) and τ_a ∈ Γ(det α). The second factor is absorbed on the other side: HeckeRing.GLn's inv_conjugate_mem_SLnZ_of_mem_ker says α⁻¹ τ_a α is again integral, so τ_a α = α · (α⁻¹ τ_a α), and the new right factor is forced into Γ₀(N) by reading off the lower-left entry of the product — which is where gcd(det α, N) = 1 is used a second time, through the lower-right entry.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Foundation.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms).

Main results

• HeckeRing.GL2.Gamma0_map_le_SLnZ: Γ₀(N) ≤ SL₂(ℤ) inside GL₂(ℚ).
• HeckeRing.GL2.doubleCoset_Gamma0_map_le_doubleCoset_SLnZ: Γ₀(N) α Γ₀(N) ⊆ Γ α Γ.
• HeckeRing.GL2.gcd_apply_one_one_eq_one: for an integral matrix with N ∣ c and determinant coprime to N, the lower-right entry is coprime to N.
• HeckeRing.GL2.doubleCoset_SLnZ_inter_Delta0_eq_doubleCoset_Gamma0_map: the equality above.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Lemma 3.29(3).

theorem HeckeRing.GL2.Gamma0_map_le_SLnZ (N : ℕ) : Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N) ≤ GLn.SLnZ 2

Γ₀(N) ≤ SL₂(ℤ) as subgroups of GL₂(ℚ): the image of any integral matrix of determinant one lies in the range of mapGL.

Stated at the unfolded (Gamma0 N).map (mapGL ℚ) so the coset layer can use it directly: the HeckeCoset types of CosetMap.lean are spelled that way, and transporting a folded containment along Gamma0Image_def at each use site would hide the canonical form.

theorem HeckeRing.GL2.doubleCoset_Gamma0_map_le_doubleCoset_SLnZ (N : ℕ) (α : GL (Fin 2) ℚ) : DoubleCoset.doubleCoset α ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ⊆ DoubleCoset.doubleCoset α ↑(GLn.SLnZ 2) ↑(GLn.SLnZ 2)

Γ₀(N) α Γ₀(N) ⊆ Γ α Γ: immediate from Γ₀(N) ≤ SL₂(ℤ).

theorem HeckeRing.GL2.gcd_apply_one_one_eq_one (N : ℕ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hAN : ↑N ∣ A 1 0) (hdet : A.det.gcd ↑N = 1) : (A 1 1).gcd ↑N = 1

If N ∣ c and det is coprime to N, then so is the lower-right entry: modulo N the determinant is a * d, so d divides a unit.

theorem HeckeRing.GL2.doubleCoset_SLnZ_inter_Delta0_eq_doubleCoset_Gamma0_map (N : ℕ) (α : GL (Fin 2) ℚ) (hα : α ∈ Delta0 N) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑α = A.map Int.cast) (hdet : A.det.gcd ↑N = 1) : DoubleCoset.doubleCoset α ↑(GLn.SLnZ 2) ↑(GLn.SLnZ 2) ∩ ↑(Delta0 N) = DoubleCoset.doubleCoset α ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

Shimura, Lemma 3.29(3). For α ∈ Δ₀(N) with gcd(det α, N) = 1, cutting the level-one double coset down to Δ₀(N) leaves exactly the Γ₀(N)-double coset: SL₂(ℤ) α SL₂(ℤ) ∩ Δ₀(N) = Γ₀(N) α Γ₀(N).

This is the prerequisite for comparing the level-one and Γ₀(N) Hecke operators at an index coprime to the level, and so for the later multiplicativity of T_n on M_k(Γ₀(N)); neither comparison nor multiplicativity is proved here — this identifies the two double cosets.