Upper-triangular representatives for a diagonal double coset

For an arbitrary tuple a of naturals, this file exhibits a family of elements of the double coset SL_n(ℤ) · diag(a) · SL_n(ℤ), indexed by the bounded entry assignments B_{ij} ∈ {0, …, a_j / a_i - 1} for i < j. The construction, its membership in the double coset, and its injectivity need no hypothesis on a at all.

Distinctness of the cosets does: when a is positive and a divisibility chain (IsDvdChain), distinct entry assignments give representatives in distinct left SL_n(ℤ)-cosets. The chain condition is what makes a_j / a_i an exact quotient, which is what turns integrality of the connecting element into the divisibility the argument runs on.

Counting the index type then bounds the number of left cosets in the double coset below by ∏_{i < j} (a_j / a_i). That count is a consequence of the distinctness proved here, not itself a declaration in this file.

The representative attached to B is defined as diag(a) · U(B), where U(B) is the unipotent upper-triangular integral matrix with off-diagonal entries B. Two things follow from that shape, and are the reason for choosing it over an entrywise definition: U(B) is upper triangular with ones on the diagonal, so det U(B) = 1 and U(B) ∈ SL_n(ℤ); and hence the representative lies in the double coset with no further argument. upperTriGL_apply_lt, upperTriGL_apply_diag and upperTriGL_apply_eq_zero_of_lt recover the entrywise description M_{ij} = a_i · B_{ij} for consumers that need it; injectivity itself does not, since upperTriGL is visibly a composition of injective maps.

Main definitions

• UpperTriEntries — the bounded entry assignments B_{ij} ∈ Fin (a j / a i) for i < j.
• unitriMat, unitriSL — the unipotent upper-triangular matrix U(B), and its packaging as an element of SL_n(ℤ).
• upperTriGL — the representative diag(a) · U(B) in GL_n(ℚ).

Main results

• upperTriGL_mem_doubleCoset — every representative lies in SL_n(ℤ) · diag(a) · SL_n(ℤ).
• unitriMat_injective, upperTriGL_injective — distinct entry assignments give distinct matrices, hence distinct representatives.
• eq_of_upperTriGL_eq_mapGL_mul_upperTriGL and eq_of_upperTriGL_mul_inv_mem_SLnZ — the representatives lie in distinct left SL_n(ℤ)-cosets: two of them are left-equivalent only when their entry assignments already agree, for a positive IsDvdChain.

The two steps behind that conclusion are also stated separately, since each is reusable: dvd_comparison_of_upperTriGL_eq_mapGL_mul_upperTriGL turns left equivalence into (a_j / a_i) ∣ C_{ij} for the comparison matrix C = U(B₁) · U(B₂)⁻¹, by conjugating the connecting element back through diag(a); and eq_of_dvd_comparison turns that divisibility into C = 1, because the entry bound B_{ij} < a_j / a_i leaves no room for a nonzero multiple, by induction on j - i.

References

The background for working with upper-triangular representatives at all is Shimura, Introduction to the Arithmetic Theory of Automorphic Functions (1971), Exercise 3.26(A), p. 65: for every α ∈ Δ one can choose representatives α_j of ΓαΓ = ⋃_j Γα_j with L_ν α_j ⊆ L_ν for the standard flag L_ν = ∑_{i ≤ ν} ℤ e_i, i.e. upper-triangular ones. Shimura leaves it as an exercise and works the n = 2 case explicitly in Prop. 3.33 (p. 70) and Prop. 3.36 (p. 72).

That exercise is motivation, not the statement proved here. It asserts only that flag-preserving representatives exist; it does not supply this bounded family B_{ij} ∈ Fin (a_j / a_i), nor the distinctness of the left cosets they occupy. Those are proved below and are not read off from the exercise.

The definitions follow the AINTLIB LeanModularForms file LeanModularForms/HeckeRIngs/GLn/CosetDecomposition.lean (Chris Birkbeck), whose module docstring cites "Shimura, Proposition 3.22" — that number is in fact Lemma 3.22, an Euler product identity, and is unrelated. The results here are new: the AINTLIB file states the definitions and the determinant, and advertises the coset results in its docstring without proving them.

@[reducible, inline]

abbrev HeckeRing.GLn.UpperTriEntries (n : ℕ) (a : Fin n → ℕ) : Type

Bounded entry assignments for upper-triangular representatives: an integer B_{ij} ∈ {0, …, a_j / a_i - 1} for each pair i < j.

Stated for an arbitrary tuple a, with no chain or positivity hypothesis: those are needed by the results, not to name the index type. The component Fin (a j / a i) is empty exactly when a j / a i = 0, which for positive a i means a j < a i.

Equations

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

def HeckeRing.GLn.unitriMat {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : Matrix (Fin n) (Fin n) ℤ

The unipotent upper-triangular integral matrix U(B): ones on the diagonal, B_{ij} above it, zeros below.

Equations

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

@[simp]

theorem HeckeRing.GLn.unitriMat_apply_lt {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) {i j : Fin n} (h : i < j) : unitriMat B i j = ↑↑(B ⟨(i, j), h⟩)

@[simp]

theorem HeckeRing.GLn.unitriMat_apply_diag {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) (i : Fin n) : unitriMat B i i = 1

@[simp]

theorem HeckeRing.GLn.unitriMat_apply_eq_zero_of_lt {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) {i j : Fin n} (h : j < i) : unitriMat B i j = 0

theorem HeckeRing.GLn.isUpperTriangular_unitriMat {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : (unitriMat B).IsUpperTriangular

@[simp]

theorem HeckeRing.GLn.det_unitriMat {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : (unitriMat B).det = 1

U(B) is upper triangular with ones on the diagonal, so its determinant is 1.

def HeckeRing.GLn.unitriSL {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : Matrix.SpecialLinearGroup (Fin n) ℤ

U(B) packaged as an element of SL_n(ℤ).

Equations

• HeckeRing.GLn.unitriSL B = ⟨HeckeRing.GLn.unitriMat B, ⋯⟩

@[simp]

theorem HeckeRing.GLn.coe_unitriSL {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : ↑(unitriSL B) = unitriMat B

noncomputable def HeckeRing.GLn.upperTriGL {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : GL (Fin n) ℚ

The upper-triangular representative diag(a) · U(B) attached to a bounded entry assignment.

Equations

• HeckeRing.GLn.upperTriGL B = HeckeRing.GLn.natDiagGL n a * (Matrix.SpecialLinearGroup.mapGL ℚ) (HeckeRing.GLn.unitriSL B)

theorem HeckeRing.GLn.upperTriGL_def {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : upperTriGL B = natDiagGL n a * (Matrix.SpecialLinearGroup.mapGL ℚ) (unitriSL B)

The defining factorisation of the representative, as a characteristic lemma: consumers can work from diag(a) · U(B) without unfolding upperTriGL.

@[simp]

theorem HeckeRing.GLn.upperTriGL_coe {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (B : UpperTriEntries n a) : ↑(upperTriGL B) = (Matrix.diagonal fun (i : Fin n) => ↑(a i)) * (unitriMat B).map Int.cast

The matrix of the representative: diag(a) · U(B) entrywise over ℚ. upperTriGL is built from natDiagGL and mapGL, so consumers that need the literal matrix — for instance to recognise the classical T_p representatives !![1, b; 0, p] at n = 2, a = ![1, p] — would otherwise unfold three definitions to get it.

theorem HeckeRing.GLn.upperTriGL_mem_doubleCoset {n : ℕ} {a : Fin n → ℕ} (B : UpperTriEntries n a) : upperTriGL B ∈ DoubleCoset.doubleCoset (natDiagGL n a) ↑(SLnZ n) ↑(SLnZ n)

Each upper-triangular representative lies in the double coset of diag(a).

@[simp]

theorem HeckeRing.GLn.upperTriGL_apply_lt {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (B : UpperTriEntries n a) {i j : Fin n} (h : i < j) : ↑(upperTriGL B) i j = ↑(a i) * ↑↑(B ⟨(i, j), h⟩)

The entrywise description of the representative above the diagonal: M_{ij} = a_i · B_{ij}.

@[simp]

theorem HeckeRing.GLn.upperTriGL_apply_diag {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (B : UpperTriEntries n a) (i : Fin n) : ↑(upperTriGL B) i i = ↑(a i)

The entrywise description on the diagonal: M_{ii} = a_i.

@[simp]

theorem HeckeRing.GLn.upperTriGL_apply_eq_zero_of_lt {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (B : UpperTriEntries n a) {i j : Fin n} (h : j < i) : ↑(upperTriGL B) i j = 0

The representative is upper triangular: entries below the diagonal vanish.

theorem HeckeRing.GLn.unitriMat_injective {n : ℕ} {a : Fin n → ℕ} : Function.Injective unitriMat

Distinct entry assignments give distinct unipotent matrices.

theorem HeckeRing.GLn.upperTriGL_injective {n : ℕ} {a : Fin n → ℕ} : Function.Injective upperTriGL

Distinct entry assignments give distinct representatives. No positivity hypothesis on a is needed: this holds even at a tuple where natDiagGL takes its junk value 1.

Distinctness of the left cosets

Two representatives lie in the same left SL_n(ℤ)-coset exactly when the conjugate diag(a)⁻¹ · S · diag(a) of the connecting element S is integral, which says (a_j / a_i) ∣ C_{ij} for the comparison matrix C = U(B₁) · U(B₂)⁻¹. The entry bound B_{ij} < a_j / a_i then forces C = 1.

theorem HeckeRing.GLn.eq_of_dvd_comparison {n : ℕ} {a : Fin n → ℕ} {B₁ B₂ : UpperTriEntries n a} (hdvd : ∀ ⦃i j : Fin n⦄, i < j → ↑(a j / a i) ∣ (unitriMat B₁ * (unitriMat B₂)⁻¹) i j) : B₁ = B₂

The divisibility criterion for equality of entry assignments: if the comparison matrix C = U(B₁) · U(B₂)⁻¹ satisfies (a_j / a_i) ∣ C_{ij} above the diagonal, then B₁ = B₂.

This is arithmetic about a hypothesised divisibility; nothing here mentions cosets. What makes that divisibility hold for two representatives in the same left SL_n(ℤ)-coset is dvd_comparison_of_upperTriGL_eq_mapGL_mul_upperTriGL, and eq_of_upperTriGL_eq_mapGL_mul_upperTriGL is the two combined.

theorem HeckeRing.GLn.dvd_comparison_of_upperTriGL_eq_mapGL_mul_upperTriGL {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) {B₁ B₂ : UpperTriEntries n a} {S : Matrix.SpecialLinearGroup (Fin n) ℤ} (hS : upperTriGL B₁ = (Matrix.SpecialLinearGroup.mapGL ℚ) S * upperTriGL B₂) {i j : Fin n} (hdvd : a i ∣ a j) : ↑(a j / a i) ∣ (unitriMat B₁ * (unitriMat B₂)⁻¹) i j

Two representatives in the same left SL_n(ℤ)-coset have comparison matrix divisible above the diagonal: (a_j / a_i) ∣ C_{ij} for C = U(B₁) · U(B₂)⁻¹. This is the divisibility that eq_of_dvd_comparison takes as a hypothesis, so the two together make distinctness a theorem about the coset relation rather than a criterion. Only a i ∣ a j is needed, at the pair asked about.

theorem HeckeRing.GLn.eq_of_upperTriGL_eq_mapGL_mul_upperTriGL {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (hchain : IsDvdChain a) {B₁ B₂ : UpperTriEntries n a} {S : Matrix.SpecialLinearGroup (Fin n) ℤ} (hS : upperTriGL B₁ = (Matrix.SpecialLinearGroup.mapGL ℚ) S * upperTriGL B₂) : B₁ = B₂

The upper-triangular representatives of a positive divisibility chain lie in pairwise distinct left SL_n(ℤ)-cosets: if two of them differ by a left factor in SL_n(ℤ), their entry assignments already agree. Equivalently, B ↦ SL_n(ℤ) · upperTriGL B is injective.

theorem HeckeRing.GLn.eq_of_upperTriGL_mul_inv_mem_SLnZ {n : ℕ} {a : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (hchain : IsDvdChain a) {B₁ B₂ : UpperTriEntries n a} (h : upperTriGL B₁ * (upperTriGL B₂)⁻¹ ∈ SLnZ n) : B₁ = B₂

The same statement phrased with the subgroup SLnZ n of GL_n(ℚ): distinct entry assignments give representatives in distinct left cosets of SL_n(ℤ).