Γ₀(N) double cosets are determined by their elementary divisors

Two elements of Δ₀(N) whose integral matrices have the same determinant and the same common divisors of entries lie in the same Γ₀(N)-double coset. No hypothesis relating the determinant to the level is needed; this is the form of Shimura's Proposition 3.32 in which the double coset is read off the matrix, and it extends the coprime-determinant case HeckeRing.GL2.doubleCoset_SLnZ_inter_Delta0_eq_doubleCoset_Gamma0_map.

A primitive witness — one no prime divides entrywise — of determinant m lies in the double coset of diag(1, m). Split m = b * c with b = gcd (m, N ^ m) collecting the primes shared with the level, so that c is coprime to N. The two-sided clearing exists_gamma0_mul_mul_coprime_upperLeft moves the witness inside its double coset until its upper-left entry is coprime to c as well as to N, hence to m, and then Shimura's 3.33 (mem_doubleCoset_natDiagGL_of_intWitness) applies. In general, dividing out the gcd d of the entries leaves a primitive witness; d is coprime to the level and central, so it can be put back on both sides.

Main results

• HeckeRing.GL2.mem_doubleCoset_natDiagGL_of_primitive: a primitive witness of determinant m lies in Γ₀(N) diag(1, m) Γ₀(N).
• HeckeRing.GL2.mem_doubleCoset_of_det_eq_of_dvd_iff: elements of Δ₀(N) with equal determinants and equal common divisors of entries share a Γ₀(N)-double coset.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Propositions 3.32 and 3.33.

theorem HeckeRing.GL2.mem_doubleCoset_natDiagGL_of_primitive (N : ℕ) [NeZero N] (m : ℕ) (x : GL (Fin 2) ℚ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑x = A.map Int.cast) (hAN : ↑N ∣ A 1 0) (hAco : (A 0 0).gcd ↑N = 1) (hdet : (↑x).det = ↑m) (hprim : ∀ (p : ℕ), Nat.Prime p → ¬(↑p ∣ A 0 0 ∧ ↑p ∣ A 0 1 ∧ ↑p ∣ A 1 0 ∧ ↑p ∣ A 1 1)) : x ∈ DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, m]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

A primitive witness lies in the double coset of diag(1, m). Let x ∈ GL₂(ℚ) have an integral matrix A with N ∣ A 1 0, upper-left entry coprime to N, determinant m, and no prime dividing all four entries. Then x ∈ Γ₀(N) diag(1, m) Γ₀(N).

theorem HeckeRing.GL2.mem_doubleCoset_of_det_eq_of_dvd_iff (N : ℕ) [NeZero N] {α β : GL (Fin 2) ℚ} (hα : α ∈ Delta0 N) (hβ : β ∈ Delta0 N) {A B : Matrix (Fin 2) (Fin 2) ℤ} (hA : ↑α = A.map Int.cast) (hB : ↑β = B.map Int.cast) (hdet : B.det = A.det) (hdvd : ∀ (e : ℤ), (∀ (i j : Fin 2), e ∣ A i j) ↔ ∀ (i j : Fin 2), e ∣ B i j) : β ∈ DoubleCoset.doubleCoset α ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

Elements of Δ₀(N) with the same elementary divisors share a Γ₀(N)-double coset. If α, β ∈ Δ₀(N) have integral matrices A, B of equal determinant, and an integer divides all entries of A exactly when it divides all entries of B, then β ∈ Γ₀(N) α Γ₀(N).