The leading coefficient of a product of diagonal double cosets

For positive divisibility chains a and b, the double coset T(a b) occurs in the product T(a) · T(b) of the integral Hecke ring of (SL_n(ℤ), Δ) with coefficient exactly one. For p-power diagonals with monotone exponent vectors e and f this is the coefficient of the leading term T(p ^ (e + f)) of T(p ^ e) · T(p ^ f); the companion statement that every other coset of the product lies strictly below it in the dominance order is HeckeRing.GLn.exists_primePowDiag_of_diagElem_mul_apply_ne_zero. Together they form the triangular expansion on which Shimura's presentation of the p-local Hecke ring as a polynomial ring rests (Theorem 3.20).

The coefficient is Shimura's multiplicity: the number of left cosets σ diag(a) SL_n(ℤ) in the double coset T(a) for which σ diag(a) τ diag(b) lies in diag(a b) SL_n(ℤ) for some τ. The coset of σ = 1 is one of them, and it is the only one by Matrix.dvd_apply_mul_of_dvd_mul_diagonal_mul_diagonal_apply: an equation σ diag(a) τ diag(b) = diag(a) diag(b) γ with σ, τ, γ in SL_n(ℤ) forces diag(a)⁻¹ σ diag(a) to be integral.

Main results

• HeckeRing.GLn.diagElem_mul_apply_diagCoset_mul: the coefficient of T(a b) in T(a) · T(b) is 1.
• HeckeRing.GLn.diagElem_primePowDiag_mul_apply_diagCoset_add: the coefficient of T(p ^ (e + f)) in T(p ^ e) · T(p ^ f) is 1.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.2, the proof of Theorem 3.20.

theorem HeckeRing.GLn.diagElem_mul_apply_diagCoset_mul {n : ℕ} {a b : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (ha' : IsDvdChain a) (hb : ∀ (i : Fin n), 0 < b i) (hb' : IsDvdChain b) : (diagElem a * diagElem b) (diagCoset (a * b)) = 1

The leading coefficient of a product of diagonal double cosets. For positive divisibility chains a and b, the double coset T(a b) occurs in T(a) · T(b) with coefficient 1.

theorem HeckeRing.GLn.diagElem_primePowDiag_mul_apply_diagCoset_add {n p : ℕ} (hp : 0 < p) {e f : Fin n → ℕ} (he : Monotone e) (hf : Monotone f) : (diagElem (primePowDiag n p e) * diagElem (primePowDiag n p f)) (diagCoset (primePowDiag n p (e + f))) = 1

The leading term of a product of p-power diagonal cosets has coefficient one. For 0 < p and monotone exponent vectors e and f, the coset T(p ^ (e + f)) occurs in T(p ^ e) · T(p ^ f) with coefficient 1.