Left Coset Decomposition for GL_n Hecke Ring

Upper-triangular coset representatives for Γ · diag(a) · Γ, where Γ = SL_n(ℤ).

For a = (a₁,...,aₙ) with a₁ | a₂ | ⋯ | aₙ, left coset representatives include upper-triangular matrices M = diag(a) · γ where γ is unipotent upper-triangular with γ_{ij} ∈ {0,...,(a_j/a_i) - 1} for i < j. These give ∏_{i<j}(a_j/a_i) distinct left cosets.

Main definitions

• UpperTriRep -- bounded entry assignment: γ_{ij} ∈ Fin (a_j / a_i) for i < j
• upperTriMat -- the upper-triangular integer matrix M_{ij} = a_i · γ_{ij}
• upperTriGL -- corresponding GL_n(ℚ) element

Main results

• upperTriMat_det -- det(M) = ∏ i, a_i
• upperTriMat_injective -- different entries produce different matrices
• upperTriGL_mem_doubleCoset -- each representative lies in Γ · diag(a) · Γ
• upperTriMat_distinct_cosets -- distinct representatives give distinct left cosets

References

• Shimura, Proposition 3.22

@[reducible, inline]

abbrev HeckeRing.GLn.UpperTriRep (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) : Type

Bounded entry assignment for upper-triangular representatives: B_{ij} ∈ Fin (a_j / a_i) for i < j.

Equations

• HeckeRing.GLn.UpperTriRep n a hdiv = ((p : { ij : Fin n × Fin n // ij.1 < ij.2 }) → Fin (a (↑p).2 / a (↑p).1))

def HeckeRing.GLn.upperTriMat (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : Matrix (Fin n) (Fin n) ℤ

Upper-triangular matrix with diagonal a and off-diagonal M_{ij} = a_i * B_{ij}.

Equations

• HeckeRing.GLn.upperTriMat n a hdiv B i j = if h : i < j then ↑(a i) * ↑↑(B ⟨(i, j), h⟩) else if i = j then ↑(a i) else 0

@[simp]

theorem HeckeRing.GLn.upperTriMat_apply_lt (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) {i j : Fin n} (h : i < j) : upperTriMat n a hdiv B i j = ↑(a i) * ↑↑(B ⟨(i, j), h⟩)

@[simp]

theorem HeckeRing.GLn.upperTriMat_apply_diag (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) (i : Fin n) : upperTriMat n a hdiv B i i = ↑(a i)

theorem HeckeRing.GLn.upperTriMat_apply_gt (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) {i j : Fin n} (h : j < i) : upperTriMat n a hdiv B i j = 0

theorem HeckeRing.GLn.upperTriMat_det (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : (upperTriMat n a hdiv B).det = ∏ i : Fin n, ↑(a i)

theorem HeckeRing.GLn.upperTriMat_det_pos (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : 0 < (upperTriMat n a hdiv B).det

theorem HeckeRing.GLn.upperTriMat_injective (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) : Function.Injective (upperTriMat n a hdiv)

noncomputable def HeckeRing.GLn.upperTriGL (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : GL (Fin n) ℚ

The upper-triangular representative as a GL_n(ℚ) element.

Equations

• HeckeRing.GLn.upperTriGL n a hpos hdiv B = Matrix.GeneralLinearGroup.mkOfDetNeZero ((HeckeRing.GLn.upperTriMat n a hdiv B).map Int.cast) ⋯

@[simp]

theorem HeckeRing.GLn.upperTriGL_val (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : ↑(upperTriGL n a hpos hdiv B) = (upperTriMat n a hdiv B).map Int.cast

theorem HeckeRing.GLn.upperTriGL_hasIntEntries (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : HasIntEntries n (upperTriGL n a hpos hdiv B)

theorem HeckeRing.GLn.upperTriGL_mem_posDetInt (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : upperTriGL n a hpos hdiv B ∈ posDetIntSubmonoid n

def HeckeRing.GLn.unipMat (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : Matrix (Fin n) (Fin n) ℤ

The unipotent upper-triangular matrix with 1 on the diagonal and B_{ij} above.

Equations

• HeckeRing.GLn.unipMat n a hdiv B i j = if h : i < j then ↑↑(B ⟨(i, j), h⟩) else if i = j then 1 else 0

theorem HeckeRing.GLn.unipMat_det (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : (unipMat n a hdiv B).det = 1

theorem HeckeRing.GLn.upperTriGL_mem_doubleCoset (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B : UpperTriRep n a hdiv) : upperTriGL n a hpos hdiv B ∈ DoubleCoset.doubleCoset (diagMat n a) ↑(SLnZSubgroup n) ↑(SLnZSubgroup n)

Each upper-triangular representative lies in Γ · diag(a) · Γ.

theorem HeckeRing.GLn.upperTriMat_distinct_cosets (n : ℕ) (a : Fin n → ℕ) (hpos : ∀ (i : Fin n), 0 < a i) (hdiv : DivChain n a) (B₁ B₂ : UpperTriRep n a hdiv) (hne : B₁ ≠ B₂) (γ : GL (Fin n) ℚ) : γ ∈ SLnZSubgroup n → upperTriGL n a hpos hdiv B₁ ≠ γ * upperTriGL n a hpos hdiv B₂

Distinct entry assignments give distinct left cosets of SL_n(ℤ).

theorem HeckeRing.GLn.upperTriRep_card (n : ℕ) (a : Fin n → ℕ) (hdiv : DivChain n a) : Fintype.card (UpperTriRep n a hdiv) = ∏ p : { ij : Fin n × Fin n // ij.1 < ij.2 }, a (↑p).2 / a (↑p).1

The number of upper-triangular representatives equals ∏_{i<j} (a_j / a_i).