The p-local Hecke ring of GL_n is a polynomial ring

Shimura's Theorem 3.20: for p prime, the p-local Hecke ring R_p = pLocalSubring n p of (SL_n(ℤ), Δ) is the polynomial ring ℤ[X₁, …, Xₙ] on the diagonal prime cosets heckeGen k = T(1, …, 1, p, …, p), with k + 1 entries equal to p. Here R_p is spanned by the double cosets of integral matrices with p-power determinant: it is the positive part of the spherical Hecke algebra of GL_n(ℚ_p), which is obtained from it by inverting the scalar coset T(p, …, p).

The proof is a leading-term argument. The monomial ∏ k, heckeGen k ^ e k is a sum of diagonal double cosets T(p ^ g) that is triangular for the dominance order of exponent vectors (TauCeti.Dominates), a dominating g when the two have the same total and every leading partial sum ∑_{j < k} a j is at most that of g:

• the leading coset T(p ^ leadingExponent e) occurs with coefficient 1;
• every coset that occurs is T(p ^ g) for a monotone g dominated by leadingExponent e.

This is proved one generator at a time, from the two halves of the statement for a product of two diagonal cosets, HeckeRing.GLn.diagElem_primePowDiag_mul_apply_diagCoset_add (the leading coefficient) and HeckeRing.GLn.exists_primePowDiag_of_diagElem_mul_apply_ne_zero (the support), since dominance is compatible with adding exponent vectors. Since HeckeRing.GLn.leadingExponent is injective with image the monotone vectors, the leading cosets of distinct monomials are distinct and every coset T(p ^ g) of R_p is a leading coset. Injectivity then follows by looking at a monomial whose leading coset is maximal, and surjectivity by induction along the dominance order.

Main results

• HeckeRing.GLn.prod_heckeGen_pow_apply_diagCoset_leadingExponent: the leading coset of a monomial occurs with coefficient 1.
• HeckeRing.GLn.exists_primePowDiag_of_prod_heckeGen_pow_apply_ne_zero: every coset of the support of a monomial is T(p ^ g) for a monotone g dominated by the leading exponent vector.
• HeckeRing.GLn.evalHom_injective, HeckeRing.GLn.range_evalHom: the generators are algebraically independent and generate R_p.
• HeckeRing.GLn.polynomialRingEquiv: Shimura, Theorem 3.20, ℤ[X₁, …, Xₙ] ≃+* R_p.

References

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

theorem HeckeRing.GLn.prod_heckeGen_pow_apply_diagCoset_leadingExponent {n p : ℕ} (hp : Nat.Prime p) (e : Fin n → ℕ) : (∏ k : Fin n, heckeGen n p k ^ e k) (diagCoset (primePowDiag n p (leadingExponent e))) = 1

The leading coset of a Hecke monomial has coefficient one. For p prime, the coset T(p ^ leadingExponent e) occurs in ∏ k, heckeGen k ^ e k with coefficient 1.

theorem HeckeRing.GLn.exists_primePowDiag_of_prod_heckeGen_pow_apply_ne_zero {n p : ℕ} (hp : Nat.Prime p) (e : Fin n → ℕ) {D : HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)} (h : (∏ k : Fin n, heckeGen n p k ^ e k) D ≠ 0) : ∃ (g : Fin n → ℕ), Monotone g ∧ D = diagCoset (primePowDiag n p g) ∧ ∑ i : Fin n, g i = ∑ i : Fin n, leadingExponent e i ∧ ∀ (k : ℕ) (hk : k ≤ n), ∑ j : Fin k, leadingExponent e (Fin.castLE hk j) ≤ ∑ j : Fin k, g (Fin.castLE hk j)

The support of a Hecke monomial lies below its leading coset. For p prime, every double coset occurring in ∏ k, heckeGen k ^ e k is T(p ^ g) for a monotone exponent vector g with total ∑ i, leadingExponent e i whose leading partial sums are at least those of leadingExponent e.

theorem HeckeRing.GLn.evalHom_injective (n : ℕ) {p : ℕ} (hp : Nat.Prime p) : Function.Injective ⇑(evalHom n p)

The generators are algebraically independent (Shimura, Theorem 3.20): for p prime, evaluation of ℤ[X₁, …, Xₙ] at the generators heckeGen k = T(1, …, 1, p, …, p) is injective.

The image of a nonzero polynomial is nonzero at the leading coset of a monomial of its support whose leading exponent vector is maximal for the dominance order: no other monomial of the support reaches that coset.

theorem HeckeRing.GLn.range_evalHom (n : ℕ) {p : ℕ} (hp : Nat.Prime p) : (evalHom n p).range = pLocalSubring n p

The generators generate R_p (Shimura, Theorem 3.20): for p prime, the polynomials in the generators heckeGen k are exactly the elements of the p-local Hecke ring.

theorem HeckeRing.GLn.evalHomLocal_injective (n : ℕ) {p : ℕ} (hp : Nat.Prime p) : Function.Injective ⇑(evalHomLocal n p)

The presentation map ℤ[X₁, …, Xₙ] → R_p is injective, for p prime.

theorem HeckeRing.GLn.evalHomLocal_surjective (n : ℕ) {p : ℕ} (hp : Nat.Prime p) : Function.Surjective ⇑(evalHomLocal n p)

The presentation map ℤ[X₁, …, Xₙ] → R_p is surjective, for p prime.

noncomputable def HeckeRing.GLn.polynomialRingEquiv (n : ℕ) {p : ℕ} (hp : Nat.Prime p) : MvPolynomial (Fin n) ℤ ≃+* ↥(pLocalSubring n p)

Shimura, Theorem 3.20: for p prime, the p-local Hecke ring R_p of GL_n is the polynomial ring ℤ[X₁, …, Xₙ] on the diagonal prime cosets heckeGen k = T(1, …, 1, p, …, p), with k + 1 entries equal to p.

@[simp]

theorem HeckeRing.GLn.polynomialRingEquiv_apply {n p : ℕ} (hp : Nat.Prime p) (f : MvPolynomial (Fin n) ℤ) : (polynomialRingEquiv n hp) f = (evalHomLocal n p) f

The presentation isomorphism is the evaluation map.