Degree Formulas for GL_n Hecke Ring

Degree formulas for the diagonal Hecke operators T(a₁,...,aₙ), including Gaussian binomial coefficients for the prime-power case.

Main definitions

• gaussianBinom q n k : the Gaussian binomial coefficient [n choose k]_q

Main results

• upperTriRep_card_le_HeckeCoset_deg : ∏_{i<j} (a_j / a_i) ≤ deg(T(a₁,...,aₙ))

Important note on degree formulas

The degree of T(a₁,...,aₙ) is not simply ∏_{i<j} (aⱼ/aᵢ). The upper-triangular representatives with fixed diagonal (a₁,...,aₙ) account for ∏_{i<j}(aⱼ/aᵢ) left cosets, but the double coset also contains representatives with permuted diagonals (those whose Hermite Normal Form has a different diagonal but the same Smith Normal Form).

Counterexample: For n = 2, a = (1, p) with p prime, the UpperTriRep count is p, but the actual degree is p + 1. The additional representative is [[p,0],[0,1]], which lies in the double coset SL₂(ℤ) · diag(1,p) · SL₂(ℤ) but has a different diagonal.

Correct formula for n = 2: deg(T(a₁,a₂)) = ψ(a₂/a₁) where ψ is the Dedekind psi function ψ(d) = d · ∏_{p | d} (1 + 1/p). For the prime-power case needed for Theorem 3.24: deg(T(pⁱ, pⁱ⁺ᵏ)) = pᵏ⁻¹(p + 1) for k ≥ 1.

References

• Shimura, Proposition 3.14, 3.18, Theorem 3.24

def HeckeRing.GLn.gaussianBinom (q m k : ℕ) : ℕ

Gaussian binomial coefficient [n choose k]_q.

Equations

• HeckeRing.GLn.gaussianBinom q m k = if k ≤ m then ∏ i ∈ Finset.range k, (q ^ (m - i) - 1) / (q ^ (k - i) - 1) else 0

theorem HeckeRing.GLn.gaussianBinom_zero_right (q m : ℕ) : gaussianBinom q m 0 = 1

theorem HeckeRing.GLn.gaussianBinom_gt (q m k : ℕ) (h : m < k) : gaussianBinom q m k = 0

theorem HeckeRing.GLn.upperTriRep_card_le_HeckeCoset_deg (n : ℕ) [NeZero n] (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) : ↑(Fintype.card (UpperTriRep n a hdiv)) ≤ HeckeCosetDeg (GLPair n) (TDiag a)

The number of upper-triangular representatives is a lower bound on the degree.

theorem HeckeRing.GLn.HeckeCoset_deg_T_diag_two_prime (p : ℕ) (hp : Nat.Prime p) (a : Fin 2 → ℕ) (ha : ∀ (i : Fin 2), 0 < a i) (hdiv : DivChain 2 a) (k : ℕ) (hk : 0 < k) (h_ratio : a 1 / a 0 = p ^ k) : HeckeCosetDeg (GLPair 2) (TDiag a) = ↑(p ^ (k - 1) * (p + 1))

For n = 2 and prime p: deg(T(p^i, p^(i+k))) = p^(k-1) * (p + 1) for k >= 1.

theorem HeckeRing.GLn.HeckeCoset_deg_T_diag_two_scalar (a : Fin 2 → ℕ) (ha : ∀ (i : Fin 2), 0 < a i) (_hdiv : DivChain 2 a) (h_eq : a 0 = a 1) : HeckeCosetDeg (GLPair 2) (TDiag a) = 1

For n = 2, scalar case: deg(T(c, c)) = 1.