Coprime representatives under the two-sided Γ₀(N) action

An element of Δ₀(N) whose integral matrix is primitive — no prime divides all four entries — can be moved by the two-sided Γ₀(N) action to a representative whose upper-left entry is coprime to a prescribed modulus c, provided c is coprime to N. The Δ₀(N) shape is preserved: the translate is still integral, its lower-left entry is still divisible by N, and its upper-left entry is still coprime to N — now coprime to c as well. (Coprime to N, not a unit in ℤ: nothing here proves the entry is ±1.)

The mechanism is local-to-global. For a single prime p ∤ N not dividing all of A, one of the four choices (l, t) ∈ {0,1}² already makes A₀₀ + l·A₁₀ + N·t·(A₀₁ + l·A₁₁) prime to p; primitivity is exactly what guarantees such a choice exists. Those independent local choices are then glued by the Chinese remainder theorem over c.primeFactors, and the entry depends on l and t only modulo p, so the glued pair inherits every local choice at once. The resulting l₀, t₀ are read off as the unipotent matrices !![1, l₀; 0, 1] and !![1, 0; N·t₀, 1], both of determinant 1 and both in Γ₀(N).

Together with exists_primitive_content_quotient, which divides out the content so that primitivity may be assumed, this is the reduction behind Shimura's Proposition 3.8 at level Γ₀(N): it is what lets a statement about Δ₀(N) double cosets be proved for coprime representatives first.

Ported from the AINTLIB LeanModularForms project (Chris Birkbeck), HeckeRIngs/GLn/CongruenceHecke/AtkinLehner.lean, declaration Gamma0_two_sided_coprime_rep_prim. Two hypotheses the source carries but never uses — membership of g in Δ₀(N), and c ∣ det A — are dropped here.

Main results

• HeckeRing.GL2.exists_gamma0_mul_mul_coprime_upperLeft: the two-sided clearing.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, Proposition 3.8.

The arithmetic core

The clearing lemma

theorem HeckeRing.GL2.exists_gamma0_mul_mul_coprime_upperLeft (N : ℕ) (g : GL (Fin 2) ℚ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑g = A.map Int.cast) (hAN : ↑N ∣ A 1 0) (hAco : (A 0 0).gcd ↑N = 1) (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) (hprim : ∀ (p : ℕ), Nat.Prime p → ↑p ∣ ↑c → ¬(↑p ∣ A 0 0 ∧ ↑p ∣ A 0 1 ∧ ↑p ∣ A 1 0 ∧ ↑p ∣ A 1 1)) : ∃ (γL : ↥(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))) (γR : ↥(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))) (A' : Matrix (Fin 2) (Fin 2) ℤ), ↑(↑γL * g * ↑γR) = A'.map Int.cast ∧ ↑N ∣ A' 1 0 ∧ (A' 0 0).gcd ↑N = 1 ∧ (A' 0 0).gcd ↑c = 1

Two-sided Γ₀(N) clearing. Let c be positive and coprime to N, and let A be an integral representative of g with N ∣ A₁₀ and gcd(A₀₀, N) = 1 which no prime dividing c divides entrywise. Then there are γL, γR ∈ Γ₀(N) whose two-sided translate γL · g · γR has an integral representative A' with the same two properties — N ∣ A'₁₀ and gcd(A'₀₀, N) = 1 — and in addition gcd(A'₀₀, c) = 1.

Primitivity is only assumed at primes dividing c, which is all the local-to-global argument consumes; a globally primitive A satisfies it a fortiori.