The Hecke ring acting on cusp forms

heckeSlashGamma1CuspFormEnd attaches a ℂ-linear endomorphism of S_k(Γ₁(N)) to a single double coset. This file extends that assignment ℤ-linearly to the whole Hecke ring 𝕋 Δ₀(N) Γ₁(N) ℤ, so that the abstract ring acts on the space of cusp forms.

The extension is Finsupp.linearCombination at the coefficient ring ℤ, so linearity in the ring element is inherited rather than reproved: map_zero and map_add apply directly. What is specific to this setting is the value on a basis element and on the ring identity, proved below. Multiplicativity — Shimura's Proposition 3.37 — is not proved here, so this is deliberately a ℤ-linear map and not yet a RingHom.

Main definitions

• heckeSlashGamma1CuspRingLinearMap: the ℤ-linear extension of heckeSlashGamma1CuspFormEnd to the Hecke ring.

Main results

• heckeSlashGamma1CuspRingLinearMap_single: the value on a basis element is the scaled operator of that double coset.
• heckeSlashGamma1CuspRingLinearMap_one: the ring identity acts by the operator of the identity double coset.

noncomputable def HeckeRing.GL2.heckeSlashGamma1CuspRingLinearMap {N : ℕ} [NeZero N] (k : ℤ) : HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)) ℤ →ₗ[ℤ] Module.End ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)

The Hecke ring acting on cusp forms: the ℤ-linear extension of heckeSlashGamma1CuspFormEnd from a single double coset to a formal ℤ-combination of them.

Multiplicativity is Shimura's Proposition 3.37 and is not available yet, so the Hecke ring acts ℤ-linearly here rather than by a RingHom.

Equations

• HeckeRing.GL2.heckeSlashGamma1CuspRingLinearMap k = Finsupp.linearCombination ℤ (HeckeRing.GL2.heckeSlashGamma1CuspFormEnd k)

@[simp]

theorem HeckeRing.GL2.heckeSlashGamma1CuspRingLinearMap_single {N : ℕ} [NeZero N] (k : ℤ) (D : HeckeCoset (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N)) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma1 N))) (c : ℤ) : (heckeSlashGamma1CuspRingLinearMap k) (HeckeCosetModule.single ℤ D c) = c • heckeSlashGamma1CuspFormEnd k D

The action on a basis element is the scaled operator of that double coset.

@[simp]

theorem HeckeRing.GL2.heckeSlashGamma1CuspRingLinearMap_one {N : ℕ} [NeZero N] (k : ℤ) : (heckeSlashGamma1CuspRingLinearMap k) 1 = heckeSlashGamma1CuspFormEnd k 1

The identity of the Hecke ring acts by the operator of the identity double coset.