The support of Hecke products

The structure constants of a product of two double cosets of the arithmetic Hecke triple of GL_n are constrained in two ways. First, they are supported on cosets whose representatives have the product determinant. Second, the elementary divisors of every coset in the support dominate those of the factors: if T(c) occurs in T(a) · T(b), then for each k the product of the first k elementary divisors of c is divisible by those of a times those of b. A representative of T(c) is P · diag(a) · Q · diag(b) · S with P, Q, S in SL_n(ℤ), so this is the divisibility of the k × k minors of such a product, Matrix.prod_castLE_mul_prod_castLE_dvd_of_mul_diagonal_mul_diagonal_mul_eq.

For prime-power diagonals T(p ^ e) and T(p ^ f) with monotone exponent vectors, the second constraint says that every coset of the support is T(p ^ g) with ∑ g = ∑ (e + f) and with leading partial sums ∑_{j < k} g j at least those of e + f. This is the support half of the triangular expansion of a product of diagonal prime-power cosets with respect to the leading diagonal T(p ^ (e + f)), on which the presentation of the p-local Hecke ring as a polynomial ring rests (Shimura, Theorem 3.20). The other half, that T(p ^ (e + f)) occurs with coefficient one, is HeckeRing.GLn.diagElem_primePowDiag_mul_apply_diagCoset_add, in GLn/LeadingCoefficient.lean.

Main results

• HeckeCoset.rep_det_eq_mul_of_structureConstants_ne_zero: the determinant of a coset in the support is the product of the determinants.
• HeckeRing.GLn.prod_castLE_mul_prod_castLE_dvd_of_diagElem_mul_apply_ne_zero: the leading elementary divisors of a coset in the support of T(a) · T(b) are divisible by those of a times those of b.
• HeckeRing.GLn.exists_primePowDiag_of_diagElem_mul_apply_ne_zero: every coset in the support of T(p ^ e) · T(p ^ f) is T(p ^ g) for a monotone g with total ∑ (e + f) whose leading partial sums dominate those of e + f.

The determinant argument generalizes the one in AINTLIB's LeanModularForms/HeckeRIngs/GLn/PolynomialRing.lean, which is used there for n = 2.

References

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

theorem HeckeCoset.rep_det_eq_mul_of_structureConstants_ne_zero {n : ℕ} [IsHeckeTriple (HeckeRing.GLn.posDetInt n) (HeckeRing.GLn.SLnZ n) (HeckeRing.GLn.SLnZ n)] (D₁ D₂ D : HeckeCoset (HeckeRing.GLn.posDetInt n) (HeckeRing.GLn.SLnZ n) (HeckeRing.GLn.SLnZ n)) (h : (HeckeCosetModule.structureConstants ℤ (HeckeRing.GLn.SLnZ n) (HeckeRing.GLn.SLnZ n) (HeckeRing.GLn.SLnZ n) D₁.rep D₂.rep) D ≠ 0) : (↑↑D.rep).det = (↑↑D₁.rep).det * (↑↑D₂.rep).det

A nonzero structure constant can occur only at a coset whose representative determinant is the product of the input representative determinants.

theorem HeckeRing.GLn.prod_castLE_mul_prod_castLE_dvd_of_diagElem_mul_apply_ne_zero {n : ℕ} {a b c : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (ha' : IsDvdChain a) (hb : ∀ (i : Fin n), 0 < b i) (hb' : IsDvdChain b) (hc : ∀ (i : Fin n), 0 < c i) (h : (diagElem a * diagElem b) (diagCoset c) ≠ 0) {k : ℕ} (hk : k ≤ n) : (∏ j : Fin k, a (Fin.castLE hk j)) * ∏ j : Fin k, b (Fin.castLE hk j) ∣ ∏ j : Fin k, c (Fin.castLE hk j)

The leading elementary divisors of a Hecke product dominate those of its factors. If the double coset T(c) occurs in T(a) · T(b), where a and b are positive divisibility chains and c is positive, then for every k ≤ n the product of the first k entries of c is divisible by the product of the first k entries of a times that of b. For k = n the two sides are the determinants, and they are equal (HeckeCoset.rep_det_eq_mul_of_structureConstants_ne_zero).

theorem HeckeRing.GLn.exists_primePowDiag_of_diagElem_mul_apply_ne_zero {n p : ℕ} (hp : Nat.Prime p) {e f : Fin n → ℕ} (he : Monotone e) (hf : Monotone f) {D : HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)} (h : (diagElem (primePowDiag n p e) * diagElem (primePowDiag n p f)) D ≠ 0) : ∃ (g : Fin n → ℕ), Monotone g ∧ D = diagCoset (primePowDiag n p g) ∧ ∑ i : Fin n, g i = ∑ i : Fin n, (e i + f i) ∧ ∀ (k : ℕ) (hk : k ≤ n), ∑ j : Fin k, (e (Fin.castLE hk j) + f (Fin.castLE hk j)) ≤ ∑ j : Fin k, g (Fin.castLE hk j)

The support of a product of p-power diagonal cosets lies above the sum of the exponents. Let p be prime and e, f monotone exponent vectors. Every double coset occurring in T(p ^ e) · T(p ^ f) is T(p ^ g) for a monotone exponent vector g with the same total ∑ i, g i = ∑ i, (e i + f i), whose leading partial sums dominate those of e + f: ∑_{j < k} (e j + f j) ≤ ∑_{j < k} g j for every k ≤ n.