The N-supported determinant case of Δ₀(N)

Gamma0/DoubleCoset.lean settles the coprime case: when gcd(det α, N) = 1, the SL₂(ℤ)-double coset of α meets Δ₀(N) in exactly the Γ₀(N)-double coset. This file handles the opposite extreme, Shimura Proposition 3.33: an element of Δ₀(N) whose determinant m divides a power of N lies in the Γ₀(N)-double coset of diag(1, m).

⚠ These two cases do not exhaust the determinants a Δ₀(N) element can have. A determinant may be neither coprime to N nor a divisor of a power of it: natDiagGL 2 ![1, 6] lies in Δ₀(2) with determinant 6, and gcd(6, 2) = 2 ≠ 1 while 6 ∤ 2 ^ k for every k. The mixed case is not treated here or in Gamma0/DoubleCoset.lean.

The proof is a column reduction. Coprimality of the upper-left entry to the determinant lets one column operation clear the upper row modulo m; the determinant identity then forces the lower-right entry to clear as well, leaving A in the left Γ₀(N)-coset of !![1, r; 0, m] for a reduced 0 ≤ r < m. Splitting that representative as diag(1, m) · !![1, r; 0, 1] moves the remaining parameter into a second Γ₀(N) factor, which is what makes the conclusion a double coset.

Main results

• HeckeRing.GL2.mem_doubleCoset_natDiagGL_of_dvd_pow: Shimura 3.33 — an element of Δ₀(N) whose determinant m divides a power of the level lies in the Γ₀(N)-double coset of diag(1, m).
• HeckeRing.GL2.mem_doubleCoset_natDiagGL_of_intWitness: the same conclusion drawn from an integral witness directly, with no Δ₀(N) hypothesis.
• HeckeRing.GL2.exists_unimodular_mul_upperTriangular: the column reduction, stated on its own.

References

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

• Ported from AINTLIB commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck, LeanModularForms/HeckeRIngs/GLn/CongruenceHecke/Props.lean, declarations dvd_lowerRight_witness, shimura_prop_3_33_gen and shimura_prop_3_33.

  Five source declarations are deliberately not ported. exists_mod_clearing is the Bézout step behind Int.exists_nonneg_lt_and_dvd_mul_sub (TauCeti/Data/Int/LinearCongruence.lean), which repackages the congruence solver ZMod.exists_dvd_sub_val_mul. diagMat_one_mem_Delta0 and diagMat_mem_Delta0_of_gcd are already on main as natDiagGL_one_mem_Delta0 and natDiagGL_mem_Delta0_of_coprime. fin2_col_scale exists only to drive the source's entrywise fin_cases/linarith verification of the final matrix identity, which is done here by factoring !![1, r; 0, m] and reusing HeckeRing.GLn.mapGL_mul_coe_eq_intMatrix. coprime_of_gcd_one_dvd_pow is Nat.Coprime.pow_right composed with Nat.Coprime.coprime_dvd_right and is used inline instead.

  The source's diagMat/Delta0_submonoid/(Gamma0_pair N).H vocabulary is natDiagGL/Delta0/(Gamma0 N).map (mapGL ℚ) here; the source's [NeZero N] instance, its β ∈ Δ₀(N) hypothesis on the general form, and its 0 < m hypothesis on both forms are dropped as unused or derivable.

theorem HeckeRing.GL2.det_eq_of_coe_eq_map_intCast (g : GL (Fin 2) ℚ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑g = A.map Int.cast) (m : ℕ) (hdet : (↑g).det = ↑m) : A.det = ↑m

The determinant of an integral witness. If A represents g ∈ GL₂(ℚ) entrywise over ℤ and g has determinant m, then A has determinant m over ℤ.

The Δ₀(N) membership predicate states the determinant on the ℚ-side while the column reduction works on the ℤ-side, so this cast bridge is needed to move between them.

theorem HeckeRing.GL2.exists_unimodular_mul_upperTriangular (N : ℕ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hAN : ↑N ∣ A 1 0) (m : ℕ) (hm_pos : 0 < m) (hdet : A.det = ↑m) (ham : (A 0 0).gcd ↑m = 1) : ∃ (L : Matrix (Fin 2) (Fin 2) ℤ) (r : ℤ), L.det = 1 ∧ ↑N ∣ L 1 0 ∧ 0 ≤ r ∧ r < ↑m ∧ A = L * !![1, r; 0, ↑m]

The upper-triangular normal form of the column reduction. An integral matrix with lower-left entry divisible by N, determinant m, and upper-left entry coprime to m, factors as L * !![1, r; 0, m] with L again of that Γ₀-shape — determinant one and lower-left entry divisible by N — and r reduced into [0, m).

This is the column reduction behind Shimura 3.33: it exhibits A in the left Γ₀(N)-coset of the upper-triangular representative !![1, r; 0, m]. No separate positivity hypothesis on det A is required beyond hm_pos and hdet, which already pin the determinant down; the source carries such a hypothesis as well and never uses it.

theorem HeckeRing.GL2.mem_doubleCoset_natDiagGL_of_intWitness (N m : ℕ) (β : GL (Fin 2) ℚ) (A : Matrix (Fin 2) (Fin 2) ℤ) (hA : ↑β = A.map Int.cast) (hAN : ↑N ∣ A 1 0) (hdet : (↑β).det = ↑m) (ham : (A 0 0).gcd ↑m = 1) : β ∈ DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, m]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

Shimura 3.33, from an integral witness. An element of GL₂(ℚ) with an integral matrix A whose lower-left entry is divisible by N, whose determinant is m, and whose upper-left entry is coprime to m, lies in the Γ₀(N)-double coset of diag(1, m).

Membership of Δ₀(N) is deliberately not assumed: the proof uses exactly the three facts about A that mem_Delta0_iff would hand over. Positivity of m is likewise not assumed — β is invertible, so its determinant is nonzero.

theorem HeckeRing.GL2.mem_doubleCoset_natDiagGL_of_dvd_pow (N m k : ℕ) (hm_dvd : m ∣ N ^ k) (β : GL (Fin 2) ℚ) (hβ : β ∈ Delta0 N) (hdet : (↑β).det = ↑m) : β ∈ DoubleCoset.doubleCoset (GLn.natDiagGL 2 ![1, m]) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ↑(Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N))

Shimura, Proposition 3.33. An element of Δ₀(N) whose determinant m divides a power of the level lies in the Γ₀(N)-double coset of diag(1, m).

This is the N-supported determinant case. Gamma0/DoubleCoset.lean settles the coprime case gcd(m, N) = 1; a determinant of neither kind is treated by neither file, as the module docstring records.