Scalar multiplication in the Γ₀(N) Hecke ring

The scalar row of the multiplication table at level N: T(c, c) · T(b₁, b₂) = T(cb₁, cb₂), and its consequence for the scalar operator, S_m · S_n = S_{mn}.

diag(c, c) is central, so its Γ₀(N)-double coset is a single right coset. Multiplying by it therefore permutes nothing and only rescales the diagonal entries, which is the level-N analogue of HeckeRing.GLn.diagElem_const_mul.

heckeTScalarGamma0_mul is unconditional: where a factor shares a factor with the level its operator vanishes, and so does the operator of the product, so the degenerate branches agree without a coprimality hypothesis. That is what lets Composite.lean identify the assembled scalar family with this one at every nonzero index.

Main results

• HeckeRing.GL2.diagElemGamma0_const_mul: T(c, c) · T(b) = T(c·b) at level N.
• HeckeRing.GL2.heckeTScalarGamma0_mul: S_m · S_n = S_{mn}, for all m and n.
• HeckeRing.GL2.heckeTScalarGamma0_pow: S_p ^ v = S_{p^v}, its iterate.

References

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

theorem HeckeRing.GL2.diagElemGamma0_const_mul (N : ℕ) [NeZero N] (c : ℕ) (b : Fin 2 → ℕ) : (diagElemGamma0 N fun (x : Fin 2) => c) * diagElemGamma0 N b = diagElemGamma0 N ((fun (x : Fin 2) => c) * b)

Scalar multiplication at level N: T(c, c) · T(b) = T(c·b), the level-N analogue of HeckeRing.GLn.diagElem_const_mul. No hypothesis is needed: where a factor is degenerate — not everywhere positive, or with head entry sharing a factor with the level — it vanishes, and so does T(c·b), whose entries and head inherit the defect.

@[simp]

theorem HeckeRing.GL2.heckeTScalarGamma0_mul (N : ℕ) [NeZero N] (m n : ℕ) : heckeTScalarGamma0 N m * heckeTScalarGamma0 N n = heckeTScalarGamma0 N (m * n)

The scalar operator is multiplicative: S_m · S_n = S_{mn}, with no hypothesis on m or n. Where either index is zero or shares a factor with the level its operator vanishes, and so does the operator of the product, so the degenerate branches agree too.

@[simp]

theorem HeckeRing.GL2.heckeTScalarGamma0_pow (N : ℕ) [NeZero N] (p v : ℕ) : heckeTScalarGamma0 N p ^ v = heckeTScalarGamma0 N (p ^ v)

The scalar operator on a prime power: S_p ^ v = S_{p^v}, the iterate of heckeTScalarGamma0_mul. At v = 0 both sides are the identity.