The ℤ-linear extension of the Hecke slash operators to the Hecke ring

heckeSlashGamma1ModularFormEnd attaches a ℂ-linear endomorphism of M_k(Γ₁(N)) to a single double coset. This file extends that assignment ℤ-linearly over the basis of the Hecke ring 𝕋 Δ₀(N) Γ₁(N) ℤ, assigning an endomorphism of M_k(Γ₁(N)) to each ring element.

This is not yet a ring action: multiplicativity is Shimura §3.4 and is not proved here, and the value on 1 is recorded only as the operator of the identity double coset, not as the identity endomorphism. What is delivered is the ℤ-linear assignment.

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. The one lemma proved here is the one specific to this setting: the value on a basis element.

Main definitions

• heckeSlashGamma1RingModularFormLinearMap: the ℤ-linear extension of heckeSlashGamma1ModularFormEnd to the Hecke ring.

Main results

• heckeSlashGamma1RingModularFormLinearMap_single: the value on a basis element is the scaled operator of that double coset. Together with map_zero/map_add and HeckeCosetModule.one_def this determines the map, so no further computation rules are restated here.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.4 (the action of the Hecke ring on automorphic forms).
• F. Diamond and J. Shurman, A first course in modular forms, §5.2.

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

The ℤ-linear extension of heckeSlashGamma1ModularFormEnd to formal ℤ-combinations of double cosets: ℤ-linear in the ring element, but not known to be multiplicative, so this is not yet a ring action.

𝕋 Δ H ℤ unfolds to HeckeCoset Δ H H →₀ ℤ carrying the transported module structure, which is why Finsupp.linearCombination applies at this type: the ascription below crosses the HeckeCosetModule wrapper.

Equations

• HeckeRing.GL2.heckeSlashGamma1RingModularFormLinearMap k = Finsupp.linearCombination ℤ (HeckeRing.GL2.heckeSlashGamma1ModularFormEnd k)

@[simp]

theorem HeckeRing.GL2.heckeSlashGamma1RingModularFormLinearMap_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 : ℤ) : (heckeSlashGamma1RingModularFormLinearMap k) (HeckeCosetModule.single ℤ D c) = c • heckeSlashGamma1ModularFormEnd k D

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