Hecke Operators on Modular Forms

Defines the action of the Hecke algebra on functions ℍ → ℂ via the slash action, and shows it preserves slash invariance.

Main definitions

• glMap — embedding GL₂(ℚ) →* GL₂(ℝ)
• heckeSlash — action of a double coset on functions via left coset representatives: T(D) f = Σᵢ f ∣[k] (σᵢδ)ᵀ where ΓδΓ = ⊔ Γ(δᵀσᵢᵀ) (Shimura Prop 3.30)
• heckeSlashInvariant — the Hecke operator preserves slash invariance

Implementation

The slash action on GL₂(ℚ) is induced from GL₂(ℝ) via monoidHomSlashAction glMap, so f ∣[k] g works directly for g : GL (Fin 2) ℚ without explicit coercion.

Left coset representatives are obtained by transposing right coset representatives: if ΓδΓ = ⊔ᵢ (σᵢδ)Γ, then ΓδΓ = ⊔ᵢ Γ(δᵀσᵢᵀ) since transpose is an anti-involution preserving Γ and fixing every double coset (GL_pair_onHeckeCoset_eq).

References

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

noncomputable def HeckeRing.GL2.glMap : GL (Fin 2) ℚ →* GL (Fin 2) ℝ

Embed GL₂(ℚ) into GL₂(ℝ) via ℚ ↪ ℝ.

Equations

• HeckeRing.GL2.glMap = Matrix.GeneralLinearGroup.map (algebraMap ℚ ℝ)

@[implicit_reducible]

noncomputable def HeckeRing.GL2.instSlashActionGL2Rat : SlashAction ℤ (GL (Fin 2) ℚ) (UpperHalfPlane → ℂ)

Slash action on GL₂(ℚ) induced from GL₂(ℝ) via the embedding ℚ ↪ ℝ. Satisfies f ∣[k] g = f ∣[k] glMap g definitionally.

Equations

• HeckeRing.GL2.instSlashActionGL2Rat = monoidHomSlashAction HeckeRing.GL2.glMap

@[reducible, inline]

noncomputable abbrev HeckeRing.GL2.tRep (D : HeckeCoset (GLn.GLPair 2)) (i : decompQuot (GLn.GLPair 2) D.rep) : GL (Fin 2) ℚ

The transposed right-coset representative: (σᵢ * δ)ᵀ = δᵀ * σᵢᵀ.

Equations

• HeckeRing.GL2.tRep D i = MulOpposite.unop ((HeckeRing.GLn.GLTransposeEquiv 2) (↑(Quotient.out i) * ↑D.rep))

noncomputable def HeckeRing.GL2.heckeSlash (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

The Hecke slash action of a double coset D on a function f : ℍ → ℂ.

Uses left coset representatives via transpose (Shimura Prop 3.30): T_k(D)(f) = Σᵢ f ∣[k] (σᵢδ)ᵀ where ΓδΓ = ⊔ᵢ (σᵢδ)Γ is the right coset decomposition. Each (σᵢδ)ᵀ = δᵀσᵢᵀ is a left coset representative, giving genuinely distinct terms f ∣[k] (δᵀσᵢᵀ).

Equations

• HeckeRing.GL2.heckeSlash k D f = ∑ i : HeckeRing.decompQuot (HeckeRing.GLn.GLPair 2) D.rep, SlashAction.map k (HeckeRing.GL2.tRep D i) f

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

The Hecke slash action distributes over addition of functions.

@[simp]

theorem HeckeRing.GL2.heckeSlash_zero (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) : heckeSlash k D 0 = 0

The Hecke slash action sends the zero function to zero.

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

The Hecke slash action commutes with scalar multiplication.

theorem HeckeRing.GL2.slash_tRep_of_mem (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (h₁ h₂ : GL (Fin 2) ℚ) (hh₁ : h₁ ∈ (GLn.GLPair 2).H) (hh₂ : h₂ ∈ (GLn.GLPair 2).H) (f : UpperHalfPlane → ℂ) (hf : ∀ γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range, SlashAction.map k γ f = f) : SlashAction.map k (MulOpposite.unop ((GLn.GLTransposeEquiv 2) (h₁ * ↑D.rep * h₂))) f = SlashAction.map k (tRep D ⟦⟨h₁, hh₁⟩⟧) f

Slashing by a transpose of h₁ * delta * h₂ with h₁, h₂ in H equals slashing by tRep D ⟦h₁⟧, using Gamma-invariance to absorb the H-elements.

theorem HeckeRing.GL2.heckeSlash_slash_invariant (k : ℤ) (D : HeckeCoset (GLn.GLPair 2)) (f : UpperHalfPlane → ℂ) (hf : ∀ γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range, SlashAction.map k γ f = f) (γ : GL (Fin 2) ℝ) (hγ : γ ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range) : SlashAction.map k γ (heckeSlash k D f) = heckeSlash k D f

The Hecke slash action preserves slash-invariance under SL₂(Z) (Shimura Prop 3.30).

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

The SlashInvariantForm obtained by applying a Hecke operator.

Equations

• HeckeRing.GL2.heckeSlashInvariant k D f = { toFun := HeckeRing.GL2.heckeSlash k D ⇑f, slash_action_eq' := ⋯ }

theorem HeckeRing.GL2.tRep_mul_anti (D₁ D₂ : HeckeCoset (GLn.GLPair 2)) (i : decompQuot (GLn.GLPair 2) D₁.rep) (j : decompQuot (GLn.GLPair 2) D₂.rep) : tRep D₂ j * tRep D₁ i = MulOpposite.unop ((GLn.GLTransposeEquiv 2) (↑(Quotient.out i) * ↑D₁.rep * (↑(Quotient.out j) * ↑D₂.rep)))

The transpose anti-homomorphism applied to the product of two coset reps: tRep D₂ j * tRep D₁ i = (σᵢδ₁ · σⱼδ₂)ᵀ.