Diagonal coset representatives for the GL_n Hecke ring

The double cosets T(a₁,...,aₙ) = SL_n(ℤ) · diag(a₁,...,aₙ) · SL_n(ℤ) attached to diagonal matrices with positive integer entries, and the elementary divisor theorem for the arithmetic Hecke triple: the map from positive divisibility chains a₁ ∣ a₂ ∣ ⋯ ∣ aₙ to double cosets in SL_n(ℤ) \ Δ / SL_n(ℤ) is a bijection, so these classes span the Hecke ring freely. Following Shimura, §3.2.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/DiagonalCosets.lean, Chris Birkbeck), on top of the matrix-level Smith normal form Matrix.exists_smith_normal_form_of_det_pos and its uniqueness Matrix.smith_normal_form_unique.

Main definitions

• natDiagGL: the diagonal matrix diag(a₁,...,aₙ) as an element of GL_n(ℚ).
• IsDvdChain: the divisibility condition a i ∣ a j for i ≤ j.
• diagCoset: the double coset SL_n(ℤ) · diag(a₁,...,aₙ) · SL_n(ℤ).
• diagElem: the Hecke ring element T(a₁,...,aₙ), the coset with coefficient 1.

Main results

• natDiagGL_const_eq_scalar, natDiagGL_const_mem_normalizer: a constant natural diagonal is scalar when positive, and normalizes every subgroup unconditionally.
• exists_diagonal_representative: every double coset of the arithmetic Hecke triple is diagCoset a for a positive divisibility chain a (Smith normal form).
• diagCoset_bijective: positive divisibility chains biject with the double cosets.
• diagCosetEquiv: that bijection as an equivalence, the canonical index of the double cosets.
• span_diagElem_eq_top: the elements T(a₁,...,aₙ) span the Hecke ring.
• diagElem_mul_of_mulMap_eq: the product criterion T(a) · T(b) = T(c), given that the coset decomposition multiplies into T(c) alone and does so with multiplicity at most one. The GL_n reading of HeckeCosetModule.mul_single_single_of_mulMap_eq, which carries the argument at the level of arbitrary Hecke cosets and coefficients.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions

noncomputable def HeckeRing.GLn.natDiagGL (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. Only positivity is needed for a meaningful value — a positive tuple that is not a divisibility chain still names its genuine diagonal coset.

Equations

• HeckeRing.GLn.natDiagGL n a = if h : ∀ (i : Fin n), 0 < a i then TauCeti.diagGL fun (i : Fin n) => Units.mk0 ↑(a i) ⋯ else 1

@[simp]

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

theorem HeckeRing.GLn.natDiagGL_coe_eq_map_intCast (n : ℕ) (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : ↑(natDiagGL n a) = (Matrix.diagonal fun (i : Fin n) => ↑(a i)).map Int.cast

The integral witness of natDiagGL. natDiagGL n a is the entrywise cast of the integral diagonal matrix with entries a.

natDiagGL_coe gives the same matrix as a ℚ-valued diagonal; this states it in the form the integral-witness API asks for, so that mapGL_mul_coe_eq_intMatrix and its relatives can be applied to a product with natDiagGL in the middle without re-deriving the cast each time.

theorem HeckeRing.GLn.hasIntEntries_natDiagGL (n : ℕ) (a : Fin n → ℕ) : HasIntEntries n (natDiagGL n a)

@[simp]

theorem HeckeRing.GLn.natDiagGL_mul (n : ℕ) (a b : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) : natDiagGL n a * natDiagGL n b = natDiagGL n (a * b)

The diagonal element is multiplicative in its tuple of entries.

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

theorem HeckeRing.GLn.natDiagGL_mem_posDetInt (n : ℕ) (a : Fin n → ℕ) : natDiagGL n a ∈ posDetInt n

Membership in Shimura's Δ is unconditional: the junk value is the identity.

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

@[simp]

theorem HeckeRing.GLn.natDiagGL_of_not_pos (n : ℕ) {a : Fin n → ℕ} (ha : ¬∀ (i : Fin n), 0 < a i) : natDiagGL n a = 1

The junk branch of natDiagGL: without positivity the value is the identity.

theorem HeckeRing.GLn.natDiagGL_comm (n : ℕ) (a b : Fin n → ℕ) : natDiagGL n a * natDiagGL n b = natDiagGL n b * natDiagGL n a

Natural diagonal matrices commute, with no positivity hypothesis: on the positive branch this is natDiagGL_mul and mul_comm of the entry tuples, and when either tuple fails positivity that factor is the junk value 1, which commutes with everything.

theorem HeckeRing.GLn.natDiagGL_const_eq_scalar (n : ℕ) {c : ℕ} (hc : 0 < c) : (natDiagGL n fun (x : Fin n) => c) = (Matrix.GeneralLinearGroup.scalar (Fin n)) (Units.mk0 ↑c ⋯)

A positive constant natural diagonal is the corresponding scalar matrix.

theorem HeckeRing.GLn.natDiagGL_const_comm (n c : ℕ) (g : GL (Fin n) ℚ) : (natDiagGL n fun (x : Fin n) => c) * g = g * natDiagGL n fun (x : Fin n) => c

A constant diagonal matrix is a scalar, hence commutes with everything — unconditionally in the constant, since c = 0 sends natDiagGL to its junk value 1.

theorem HeckeRing.GLn.natDiagGL_const_mem_normalizer (n c : ℕ) (Γ : Subgroup (GL (Fin n) ℚ)) : (natDiagGL n fun (x : Fin n) => c) ∈ Subgroup.normalizer ↑Γ

A constant natural diagonal normalizes every subgroup of GLₙ(ℚ): it is central.

@[simp]

theorem HeckeRing.GLn.natDiagGL_one (n : ℕ) : (natDiagGL n fun (x : Fin n) => 1) = 1

def HeckeRing.GLn.IsDvdChain {n : ℕ} (a : Fin n → ℕ) : Prop

The divisibility chain condition on natural-number sequences: entries divide all later entries. Equivalent to the successive condition a₁ ∣ a₂ ∣ ⋯ ∣ aₙ by transitivity of divisibility.

Equations

• HeckeRing.GLn.IsDvdChain a = ∀ ⦃i j : Fin n⦄, i ≤ j → a i ∣ a j

@[simp]

theorem HeckeRing.GLn.isDvdChain_iff {n : ℕ} {a : Fin n → ℕ} : IsDvdChain a ↔ ∀ ⦃i j : Fin n⦄, i ≤ j → a i ∣ a j

Elimination and introduction for the sealed definition IsDvdChain.

theorem HeckeRing.GLn.isDvdChain_const (n c : ℕ) : IsDvdChain fun (x : Fin n) => c

theorem HeckeRing.GLn.isDvdChain_mul (n : ℕ) {a b : Fin n → ℕ} (ha : IsDvdChain a) (hb : IsDvdChain b) : IsDvdChain (a * b)

The pointwise product of two divisibility chains is a divisibility chain. Scaling by a constant c is the case where b is the constant function, with hb := isDvdChain_const n c.

@[reducible, inline]

abbrev HeckeRing.GLn.CanonicalDiagonal (n : ℕ) : Type

The positive divisibility chains of length n: the parameter space of the diagonal double cosets.

Equations

• HeckeRing.GLn.CanonicalDiagonal n = { a : Fin n → ℕ // (∀ (i : Fin n), 0 < a i) ∧ HeckeRing.GLn.IsDvdChain a }

noncomputable def HeckeRing.GLn.diagCoset {n : ℕ} (a : Fin n → ℕ) : HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)

T(a₁,...,aₙ) = Γ · diag(a₁,...,aₙ) · Γ as a double coset of the arithmetic Hecke triple. The positivity hypothesis belongs in lemmas, not the definition; the value is junk when it fails.

Equations

• HeckeRing.GLn.diagCoset a = HeckeCoset.mk (HeckeRing.GLn.SLnZ n) (HeckeRing.GLn.SLnZ n) ⟨HeckeRing.GLn.natDiagGL n a, ⋯⟩

noncomputable def HeckeRing.GLn.diagElem {n : ℕ} (a : Fin n → ℕ) : IntegralHeckeRing n

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

Equations

• HeckeRing.GLn.diagElem a = HeckeCosetModule.single ℤ (HeckeRing.GLn.diagCoset a) 1

@[simp]

theorem HeckeRing.GLn.diagCoset_toSet {n : ℕ} (a : Fin n → ℕ) : (diagCoset a).toSet = DoubleCoset.doubleCoset (natDiagGL n a) ↑(SLnZ n) ↑(SLnZ n)

The underlying set of diagCoset a is the double coset of natDiagGL n a.

theorem HeckeRing.GLn.diagCoset_def {n : ℕ} (a : Fin n → ℕ) : diagCoset a = HeckeCoset.mk (SLnZ n) (SLnZ n) ⟨natDiagGL n a, ⋯⟩

Defining equation for the sealed diagCoset.

theorem HeckeRing.GLn.exists_rep_diagCoset_eq_mul_natDiagGL_mul {n : ℕ} (a : Fin n → ℕ) : ∃ h₁ ∈ SLnZ n, ∃ h₂ ∈ SLnZ n, ↑(diagCoset a).rep = h₁ * natDiagGL n a * h₂

The chosen representative of a diagonal coset decomposes as h₁ · diag(a) · h₂ with h₁, h₂ ∈ SL_n(ℤ).

@[simp]

theorem HeckeRing.GLn.diagCoset_rep_det {n : ℕ} (a : Fin n → ℕ) (ha : ∀ (i : Fin n), 0 < a i) : (↑↑(diagCoset a).rep).det = ∏ i : Fin n, ↑(a i)

The determinant of a diagonal coset's chosen representative is ∏ i, a i, the same as that of natDiagGL n a itself, since the two differ only by factors from SLₙ(ℤ).

This is the form in which determinants of products written through chosen double-coset representatives are computed, where the representative and not the diagonal matrix is what occurs.

theorem HeckeRing.GLn.diagElem_def {n : ℕ} (a : Fin n → ℕ) : diagElem a = HeckeCosetModule.single ℤ (diagCoset a) 1

Defining equation for the sealed diagElem.

@[simp]

theorem HeckeRing.GLn.diagCoset_one {n : ℕ} : (diagCoset fun (x : Fin n) => 1) = 1

@[simp]

theorem HeckeRing.GLn.diagElem_one {n : ℕ} : (diagElem fun (x : Fin n) => 1) = 1

The identity normal form: the diagonal Hecke element of the all-ones tuple is 1.

@[simp]

theorem HeckeRing.GLn.diagCoset_of_not_pos {n : ℕ} {a : Fin n → ℕ} (ha : ¬∀ (i : Fin n), 0 < a i) : diagCoset a = 1

The junk normal form: a tuple that is not everywhere positive gives the identity double coset, matching the junk value of natDiagGL.

@[simp]

theorem HeckeRing.GLn.diagElem_of_not_pos {n : ℕ} {a : Fin n → ℕ} (ha : ¬∀ (i : Fin n), 0 < a i) : diagElem a = 1

The junk normal form of the Hecke-ring element.

theorem HeckeRing.GLn.diagCoset_eq_iff {n : ℕ} (a b : Fin n → ℕ) : diagCoset a = diagCoset b ↔ DoubleCoset.doubleCoset (natDiagGL n a) ↑(SLnZ n) ↑(SLnZ n) = DoubleCoset.doubleCoset (natDiagGL n b) ↑(SLnZ n) ↑(SLnZ n)

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

theorem HeckeRing.GLn.exists_diagonal_representative {n : ℕ} (D : HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)) : ∃ (a : Fin n → ℕ), (∀ (i : Fin n), 0 < a i) ∧ IsDvdChain a ∧ D = diagCoset a

Existence of diagonal representatives (Smith normal form): every double coset of the arithmetic Hecke triple is diagCoset a for a positive divisibility chain a₁ ∣ a₂ ∣ ⋯ ∣ aₙ.

theorem HeckeRing.GLn.eq_of_diagCoset_eq {n : ℕ} {a b : Fin n → ℕ} (ha : ∀ (i : Fin n), 0 < a i) (hb : ∀ (i : Fin n), 0 < b i) (hda : IsDvdChain a) (hdb : IsDvdChain b) (heq : diagCoset a = diagCoset b) : a = b

Uniqueness of elementary divisors: the entries of a diagonal representative with a divisibility chain are uniquely determined by the double coset.

theorem HeckeRing.GLn.diagCoset_bijective {n : ℕ} : Function.Bijective fun (a : CanonicalDiagonal n) => diagCoset ↑a

Classification of the double cosets (Shimura §3.2): positive divisibility chains biject with the double cosets of the arithmetic Hecke triple.

noncomputable def HeckeRing.GLn.diagCosetEquiv {n : ℕ} : CanonicalDiagonal n ≃ HeckeCoset (posDetInt n) (SLnZ n) (SLnZ n)

The canonical index of the double cosets (Shimura §3.2): the positive divisibility chains index the double cosets of the arithmetic Hecke triple, so they may be used directly as the index type and the inverse gives each coset its canonical diagonal.

Equations

• HeckeRing.GLn.diagCosetEquiv = Equiv.ofBijective (fun (a : HeckeRing.GLn.CanonicalDiagonal n) => HeckeRing.GLn.diagCoset ↑a) ⋯

@[simp]

theorem HeckeRing.GLn.diagCosetEquiv_apply {n : ℕ} (a : CanonicalDiagonal n) : diagCosetEquiv a = diagCoset ↑a

theorem HeckeRing.GLn.span_diagElem_eq_top {n : ℕ} : Submodule.span ℤ (Set.range fun (a : CanonicalDiagonal n) => diagElem ↑a) = ⊤

The Hecke ring of the arithmetic triple is spanned by the diagonal double coset elements T(a₁,...,aₙ) with positive entries and divisibility chain.

theorem HeckeRing.GLn.diagElem_mul_of_mulMap_eq {n : ℕ} [NeZero n] (a b c : Fin n → ℕ) (hmulMap : ∀ (p : DoubleCoset.DecompQuotient (SLnZ n) (SLnZ n) ↑(diagCoset a).rep × DoubleCoset.DecompQuotient (SLnZ n) (SLnZ n) ↑(diagCoset b).rep), HeckeCoset.mulMap (SLnZ n) (SLnZ n) (SLnZ n) (diagCoset a).rep (diagCoset b).rep p = diagCoset c) (hmul : DoubleCoset.multiplicity (SLnZ n) (SLnZ n) (SLnZ n) ↑(diagCoset a).rep ↑(diagCoset b).rep ↑(diagCoset c).rep ≤ 1) : diagElem a * diagElem b = diagElem c

The product criterion for diagonal Hecke elements. If every pair in the coset decomposition of T(a) · T(b) multiplies into the single double coset T(c), and T(c) occurs there with multiplicity at most one, then T(a) · T(b) = T(c).

This is the structure-constant computation shared by every "a product of diagonal elements is again diagonal" result: the two hypotheses are all that vary between them. Both the scalar product diagElem_const_mul (Shimura 3.17) and the coprime product diagElem_mul_of_coprime (Shimura 3.16) are this lemma applied to their own inputs.