Documentation

TauCeti.NumberTheory.HeckeRing.GLn.ScalarMul

Scalar multiplication in the GL_n Hecke ring #

One row of the multiplication table of the integral Hecke ring of the arithmetic Hecke triple (Shimura, Proposition 3.17): the scalar double coset T(c, …, c) has degree 1, so multiplying by it merely rescales diagonal cosets, T(c, …, c) · T(b₁, …, bₙ) = T(cb₁, …, cbₙ).

Degree one is what makes this elementary: the double coset of a scalar matrix is a single left coset, so the convolution has exactly one term and the structure constant is 1. The mirror identity then follows from commutativity of the Hecke ring rather than a second multiplicity computation.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GLn/CoprimeMul.lean, Chris Birkbeck), scalar row.

Main results #

References #

source
@[simp]
theorem HeckeRing.GLn.diagElem_const_mul (n : ℕ) [NeZero n] (c : ℕ) (hc : 0 < c) (b : Fin n → ℕ) (hb : ∀ (i : Fin n), 0 < b i) :
(diagElem fun (x : Fin n) => c) * diagElem b = diagElem ((fun (x : Fin n) => c) * b)

Scalar multiplication in the Hecke ring (Shimura, Proposition 3.17): T(c,...,c) · T(b) = T(c·b).

source
@[simp]
theorem HeckeRing.GLn.diagElem_mul_const (n : ℕ) [NeZero n] (b : Fin n → ℕ) (hb : ∀ (i : Fin n), 0 < b i) (c : ℕ) (hc : 0 < c) :
(diagElem b * diagElem fun (x : Fin n) => c) = diagElem (b * fun (x : Fin n) => c)

The scalar product, on the right: T(b) · T(c,...,c) = T(b·c). The Hecke ring of GL_n is commutative (transposition fixes every diagonal double coset), so this is the left-hand case read backwards.

source
@[simp]
theorem HeckeRing.GLn.diagElem_const_pow (n : ℕ) [NeZero n] (c : ℕ) (hc : 0 < c) (k : ℕ) :
(diagElem fun (x : Fin n) => c) ^ k = diagElem fun (x : Fin n) => c ^ k

T(c, …, c)^k = T(c^k, …, c^k): the scalar double cosets are closed under powers, the iterate of diagElem_const_mul.