Coprime multiplication in the GL_n Hecke ring

One row of the multiplication table of the integral Hecke ring of the arithmetic Hecke triple (Shimura, Proposition 3.16): when the determinants ∏ aᵢ, ∏ bᵢ are coprime, the product of the two diagonal double cosets is again a single diagonal coset, T(a) · T(b) = T(a * b).

The two levels differ in what they assume. The set-level results — the double-coset statements and their supporting lemmas — carry ∀ i, 0 < a i explicitly, because natDiagGL sends a tuple with a zero entry to its junk value 1 and those statements are about genuine diagonal representatives. The ring-level theorem diagElem_mul_of_coprime needs no positivity at all: on a tuple with a zero entry both sides degenerate, and coprimality forces the other tuple to be all ones (a zero entry makes that determinant 0, and Nat.Coprime 0 m holds only for m = 1), so the identity survives. It does assume [NeZero n], which is what the arithmetic Hecke triple instance — and hence multiplication in IntegralHeckeRing n — requires.

The scalar row (Shimura 3.17) lives in GLn/ScalarMul.lean.

The coprime case runs on a Chinese-remainder factorization of SL_n(ℤ): modulo coprime p, q an element splits as a product of one element congruent to the identity mod p and one congruent to the identity mod q (Matrix.SpecialLinearGroup.exists_mul_modEq_one_of_coprime), which is what makes the two diagonal sandwiches commute past each other.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CoprimeMul.lean, Chris Birkbeck).

Main results

• HeckeRing.GLn.mul_mem_doubleCoset_of_coprime: the set-level statement — for positive tuples with coprime determinants, a product of representatives lies in the double coset of the product tuple.
• HeckeRing.GLn.diagElem_mul_of_coprime: the ring-level statement — T(a) · T(b) = T(a * b) from coprimality alone, given [NeZero n]; the zero-entry case degenerates as described above.

References

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

Conjugating congruent elements across the diagonal

An element of SL_n(ℤ) congruent to 1 modulo the full diagonal product conjugates across natDiagGL n a — on either side — to an integral matrix of determinant one.

theorem HeckeRing.GLn.mul_mem_doubleCoset_of_coprime (n : ℕ) (a b : Fin n → ℕ) (ha_pos : ∀ (i : Fin n), 0 < a i) (hb_pos : ∀ (i : Fin n), 0 < b i) (hcop : (∏ i : Fin n, a i).Coprime (∏ i : Fin n, b i)) (τ : Matrix.SpecialLinearGroup (Fin n) ℤ) : natDiagGL n a * (Matrix.SpecialLinearGroup.mapGL ℚ) τ * natDiagGL n b ∈ DoubleCoset.doubleCoset (natDiagGL n (a * b)) ↑(SLnZ n) ↑(SLnZ n)

The set-level coprime product (Shimura, Proposition 3.16, key step): sandwiching any τ ∈ SL_n(ℤ) between the diagonals of a and b stays inside the double coset of the diagonal of a * b, when the determinants are coprime.

theorem HeckeRing.GLn.diagElem_mul_of_coprime (n : ℕ) [NeZero n] (a b : Fin n → ℕ) (hcop : (∏ i : Fin n, a i).Coprime (∏ i : Fin n, b i)) : diagElem a * diagElem b = diagElem (a * b)

Coprime product in the integral GL_n Hecke ring (Shimura, Proposition 3.16): T(a) · T(b) = T(a * b) whenever the determinants ∏ aᵢ, ∏ bᵢ are coprime.

Coprimality is the only hypothesis. natDiagGL sends a tuple with a zero entry to its junk value 1, and coprimality forces the other tuple to be all ones there: a zero entry makes that determinant 0, and Nat.Coprime 0 m holds only for m = 1. Both sides then collapse to the same element.