Hecke Operators as Endomorphisms of Modular Forms

Constructs the Hecke operator T(D) as an endomorphism of ModularForm 𝒮ℒ k, proving holomorphicity, linearity, and boundedness at cusps.

Main definitions

• heckeOperator — T(D) : ModularForm 𝒮ℒ k → ModularForm 𝒮ℒ k
• heckeOperatorLinear — T(D) as a ℂ-linear map
• heckeOperator_comp — composition corresponds to Hecke algebra multiplication

References

• Shimura, Introduction to the Arithmetic Theory of Automorphic Functions, §3.4

instance HeckeRing.GL2.instHasDetOneFinOfNatNatRealRangeSpecialLinearGroupIntGeneralLinearGroupMapGL_leanPool : (Matrix.SpecialLinearGroup.mapGL ℝ).range.HasDetOne

𝒮ℒ has determinant 1: all elements come from SL₂(ℤ).

theorem HeckeRing.GL2.heckeSlash_holomorphic (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : UpperHalfPlane → ℂ) (hf : MDiff f) : MDiff (heckeSlash k D f)

The Hecke slash action preserves holomorphicity.

theorem HeckeRing.GL2.glMap_smul_isCusp (A : GL (Fin 2) ℚ) {c : OnePoint ℝ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : IsCusp (glMap A • c) (Matrix.SpecialLinearGroup.mapGL ℝ).range

GL₂(ℚ) maps cusps of 𝒮ℒ to cusps: the Möbius action preserves ℙ¹(ℚ).

theorem HeckeRing.GL2.heckeSlash_bdd_at_cusps (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) {c : OnePoint ℝ} (hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range) : c.IsBoundedAt (heckeSlash k D ⇑f) k

The Hecke slash action preserves boundedness at cusps.

noncomputable def HeckeRing.GL2.heckeOperator (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

The Hecke operator T(D) on modular forms, preserving slash invariance and holomorphicity.

Equations

• HeckeRing.GL2.heckeOperator k D f = { toSlashInvariantForm := HeckeRing.GL2.heckeSlashInvariant k D f.toSlashInvariantForm, holo' := ⋯, bdd_at_cusps' := ⋯ }

theorem HeckeRing.GL2.heckeSlash_neg (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : UpperHalfPlane → ℂ) : heckeSlash k D (-f) = -heckeSlash k D f

Hecke slash of negation.

noncomputable def HeckeRing.GL2.heckeOperatorLinear (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k →ₗ[ℂ] ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

The Hecke operator T(D) as a ℂ-linear map on modular forms.

Equations

• HeckeRing.GL2.heckeOperatorLinear k D = { toFun := HeckeRing.GL2.heckeOperator k D, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HeckeRing.GL2.heckeSlashExt (k : ℤ) (T : GLn.HeckeAlgebra 2) (f : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

The extended Hecke slash action: extends heckeSlash by ℤ-linearity from single double cosets HeckeCoset to formal sums 𝕋 (GLPair 2) ℤ (the full Hecke algebra). heckeSlashExt k T f = T.sum (fun D c => c • heckeSlash k D f).

Equations

• HeckeRing.GL2.heckeSlashExt k T f = Finsupp.sum T fun (D : HeckeRing.HeckeCoset (HeckeRing.GLn.GLPair 2)) (c : ℤ) => c • HeckeRing.GL2.heckeSlash k D f

theorem HeckeRing.GL2.heckeSlashExt_single (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : UpperHalfPlane → ℂ) : heckeSlashExt k (Finsupp.single D 1) f = heckeSlash k D f

The extended action on a single double coset recovers heckeSlash.

theorem HeckeRing.GL2.heckeOperator_comp (k : ℤ) (D₁ D₂ : HeckeCoset (GLn.GLPair 2)) (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ⇑(heckeOperator k D₁ (heckeOperator k D₂ f)) = heckeSlashExt k (TSingle (GLn.GLPair 2) ℤ D₂ 1 * TSingle (GLn.GLPair 2) ℤ D₁ 1) ⇑f

Composing Hecke operators corresponds to Hecke algebra multiplication (Shimura Proposition 3.30): T(D₁)(T(D₂)(f)) = (T(D₂) · T(D₁))(f).