Diagonal Coset Representatives for GL_n Hecke Ring

Defines the double coset elements T(a₁,...,aₙ) corresponding to diagonal matrices diag[a₁,...,aₙ] in the Hecke ring, and proves that every double coset has a diagonal representative (elementary divisor theorem / Smith normal form).

Main definitions

• diagMat — diagonal matrix diag[a₁,...,aₙ] as element of GL_n(ℚ)
• DivChain — the divisibility chain condition a₁ | a₂ | ⋯ | aₙ
• TDiag — double coset Γ · diag[a₁,...,aₙ] · Γ
• TElem — Hecke ring basis element T(a₁,...,aₙ) with coefficient 1

Main results

• exists_diagonal_representative — every double coset has a diagonal representative with the divisibility chain a₁ | a₂ | ⋯ | aₙ (Smith normal form)
• diagonal_representative_unique — uniqueness of elementary divisors
• T_diag_span — T(a₁,...,aₙ) elements span the Hecke ring

References

• Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §3.2

noncomputable def HeckeRing.GLn.diagMat (n : ℕ) (a : Fin n → ℕ) : GL (Fin n) ℚ

The diagonal GL_n(ℚ) element diag(a₁,...,aₙ) with positive natural number entries. Returns 1 (the identity matrix) when the positivity condition ∀ i, 0 < a i fails; this is a junk value that simplifies the API by avoiding an explicit positivity argument.

Equations

• HeckeRing.GLn.diagMat n a = if h : ∀ (i : Fin n), 0 < a i then Matrix.GeneralLinearGroup.mkOfDetNeZero (Matrix.diagonal fun (i : Fin n) => ↑(a i)) ⋯ else 1

@[simp]

theorem HeckeRing.GLn.diagMat_val (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : ↑(diagMat n a) = Matrix.diagonal fun (i : Fin n) => ↑(a i)

theorem HeckeRing.GLn.diagMat_hasIntEntries (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : HasIntEntries n (diagMat n a)

theorem HeckeRing.GLn.diagMat_det_pos (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : 0 < (↑(diagMat n a)).det

theorem HeckeRing.GLn.diagMat_mem_posDetInt (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : diagMat n a ∈ posDetIntSubmonoid n

theorem HeckeRing.GLn.diagMat_det (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : (↑(diagMat n a)).det = ∏ i : Fin n, ↑(a i)

theorem HeckeRing.GLn.diagMat_one (n : ℕ) : (diagMat n fun (x : Fin n) => 1) = 1

noncomputable def HeckeRing.GLn.diagMatDelta (n : ℕ) [NeZero n] (a : Fin n → ℕ) : ↥(GLPair n).Δ

The diagonal matrix diag(a₁,...,aₙ) as an element of Shimura's Δ.

Equations

• HeckeRing.GLn.diagMatDelta n a = if h : ∀ (i : Fin n), 0 < a i then ⟨HeckeRing.GLn.diagMat n a, ⋯⟩ else ⟨1, ⋯⟩

@[simp]

theorem HeckeRing.GLn.diagMat_delta_val (n : ℕ) [NeZero n] (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : ↑(diagMatDelta n a) = diagMat n a

def HeckeRing.GLn.DivChain (n : ℕ) (a : Fin n → ℕ) : Prop

The divisibility chain condition a₁ | a₂ | ... | aₙ for positive integer sequences.

Equations

• HeckeRing.GLn.DivChain n a = ∀ (i : ℕ) (hi : i + 1 < n), a ⟨i, ⋯⟩ ∣ a ⟨i + 1, hi⟩

theorem HeckeRing.GLn.divChain_const (n c : ℕ) : DivChain n fun (x : Fin n) => c

theorem HeckeRing.GLn.divChain_dvd (n : ℕ) {a : Fin n → ℕ} (ha : DivChain n a) {i j : Fin n} (hij : i ≤ j) : a i ∣ a j

Transitivity of the divisibility chain: a i ∣ a j whenever i ≤ j.

theorem HeckeRing.GLn.divChain_div_pos (n : ℕ) {a : Fin n → ℕ} (hpos : ∀ (i : Fin n), 0 < a i) (ha : DivChain n a) {i j : Fin n} (hij : i ≤ j) : 0 < a j / a i

The quotient a j / a i is positive when i ≤ j in a divisibility chain.

noncomputable def HeckeRing.GLn.TDiag {n : ℕ} [NeZero n] (a : Fin n → ℕ) : HeckeCoset (GLPair n)

T(a₁,...,aₙ) = Γ · diag[a₁,...,aₙ] · Γ as a double coset. Hypotheses ha (positivity) and hdiv (divisibility chain) belong in lemmas, not the definition; the result is junk when they fail.

Equations

• HeckeRing.GLn.TDiag a = ⟦HeckeRing.GLn.diagMatDelta n a⟧

noncomputable def HeckeRing.GLn.TElem {n : ℕ} [NeZero n] (a : Fin n → ℕ) : HeckeAlgebra n

T(a₁,...,aₙ) as a Hecke ring element with coefficient 1.

Equations

• HeckeRing.GLn.TElem a = Finsupp.single (HeckeRing.GLn.TDiag a) 1

theorem HeckeRing.GLn.T_diag_rep_mem_doubleCoset {n : ℕ} [NeZero n] (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : ↑(TDiag a).rep ∈ DoubleCoset.doubleCoset (diagMat n a) ↑(GLPair n).H ↑(GLPair n).H

The representative of TDiag lies in the double coset of diagMat.

theorem HeckeRing.GLn.T_diag_rep_decompose {n : ℕ} [NeZero n] (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : ∃ L ∈ (GLPair n).H, ∃ R ∈ (GLPair n).H, ↑(TDiag a).rep = L * diagMat n a * R

Decompose the TDiag representative as L * diagMat * R with L, R in H.

theorem HeckeRing.GLn.T_diag_ones {n : ℕ} [NeZero n] : (TDiag fun (x : Fin n) => 1) = HeckeCoset.one (GLPair n)

theorem HeckeRing.GLn.T_diag_eq_iff {n : ℕ} [NeZero n] (a b : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) : TDiag a = TDiag b ↔ DoubleCoset.doubleCoset (diagMat n a) ↑(SLnZSubgroup n) ↑(SLnZSubgroup n) = DoubleCoset.doubleCoset (diagMat n b) ↑(SLnZSubgroup n) ↑(SLnZSubgroup n)

Two diagonal double cosets are equal iff the underlying double cosets in GL_n(ℚ) coincide.

noncomputable def HeckeRing.GLn.transvectionGL (n : ℕ) {i j : Fin n} (hij : i ≠ j) (c : ℤ) : GL (Fin n) ℚ

An elementary transvection I + c * E_{ij} as an element of GL_n(ℚ).

Equations

• HeckeRing.GLn.transvectionGL n hij c = Matrix.GeneralLinearGroup.mkOfDetNeZero ({ i := i, j := j, hij := hij, c := c }.toMatrix.map Int.cast) ⋯

theorem HeckeRing.GLn.transvectionGL_hasIntEntries (n : ℕ) {i j : Fin n} (hij : i ≠ j) (c : ℤ) : HasIntEntries n (transvectionGL n hij c)

theorem HeckeRing.GLn.transvectionGL_mem_SLnZ (n : ℕ) {i j : Fin n} (hij : i ≠ j) (c : ℤ) : transvectionGL n hij c ∈ SLnZSubgroup n

theorem HeckeRing.GLn.exists_diagonal_of_posdet (n : ℕ) (A : Matrix (Fin n) (Fin n) ℤ) (hdet : 0 < A.det) : ∃ (d : Fin n → ℤ) (_ : ∀ (i : Fin n), 0 < d i) (L : Matrix.SpecialLinearGroup (Fin n) ℤ) (R : Matrix.SpecialLinearGroup (Fin n) ℤ), ↑L * A * ↑R = Matrix.diagonal d

Every integer matrix with positive determinant is SL_n(ℤ)-equivalent to a positive diagonal.

theorem HeckeRing.GLn.exists_diagonal_representative (n : ℕ) [NeZero n] (α : ↥(GLPair n).Δ) : ∃ (a : Fin n → ℕ) (_ : ∀ (i : Fin n), 0 < a i) (_ : DivChain n a), ⟦α⟧ = TDiag a

Every element of Delta has a diagonal representative with divisibility chain (Smith normal form).

theorem HeckeRing.GLn.diagonal_representative_unique (n : ℕ) [NeZero n] (a b : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) (hda : DivChain n a) (hdb : DivChain n b) (heq : TDiag a = TDiag b) : a = b

The elementary divisors are uniquely determined by the double coset.

theorem HeckeRing.GLn.T_diag_span (n : ℕ) [NeZero n] (f : HeckeAlgebra n) : ∃ (S : Finset { p : Fin n → ℕ // (∀ (i : Fin n), 0 < p i) ∧ DivChain n p }) (c : ↥S → ℤ), f = ∑ s ∈ S.attach, c s • TElem ↑↑s

The Hecke algebra is spanned by diagonal double coset elements T(a₁,...,aₙ).