The degree of a constant diagonal double coset

A constant tuple a = (c, ..., c) has natDiagGL n a a scalar matrix, which is central in GL_n(ℚ) and so normalizes SL_n(ℤ); the double coset T(c, ..., c) is therefore a single coset and deg T(c, ..., c) = 1, at every rank.

The rank-two computation deg T(a₀, a₁) = [SL₂(ℤ) : Γ₀(a₁ / a₀)], which is not rank-general, is in TauCeti/NumberTheory/HeckeRing/GL2/DiagonalCosetDegree.lean.

Main results

• degree_diagCoset_const: deg T(c, ..., c) = 1, at every rank and for every c : ℕ — unconditionally, since a non-positive entry sends natDiagGL to its junk value 1, whose double coset is the identity.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/Degree.lean, Chris Birkbeck), keeping only the rank-general constant case; the rank-two computation is split into GL2/DiagonalCosetDegree.lean.

References

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

@[simp]

theorem HeckeRing.GLn.degree_diagCoset_const (n c : ℕ) : (diagCoset fun (x : Fin n) => c).degree = 1

The constant degree: a constant diagonal matrix is scalar, hence central, so its double coset is a single coset and deg T(c, ..., c) = 1.

The statement is unconditional in c: for c = 0 the value comes from natDiagGL's junk branch, which is 1, whose double coset is the identity — not from centrality.