Scalar cosets in the nebentypus Hecke action

This file identifies the action of the scalar double coset Γ₀(N) diag(c, c) Γ₀(N) on functions, modular forms, and cusp forms of nebentypus χ. Since the scalar matrix normalizes Γ₀(N), its double coset has one right coset. The twisting character reads its upper-left entry as χ(c), while the weight-k slash action contributes c ^ (k - 2). Consequently the scalar Hecke generator acts by

(χ (ZMod.unitOfCoprime c hcN) : ℂ) * (c : ℂ) ^ (k - 2).

The factor is χ(c), not χ(c)⁻¹: the twisted slash sum is written using right-coset representatives in Δ₀(N) and weights them by delta0NebentypusChar, whose value on the scalar representative is its upper-left unit c.

That scalar is what Prime/Recurrence.lean spends to turn the Hecke ring's prime-power recurrence into a recurrence of operators on the character spaces.

Main results

• HeckeRing.GL2.twistedHeckeSlashSumCharEnd_diagCosetGamma0_const: the scalar double coset acts by the expected scalar on the function character space.
• HeckeRing.GL2.twistedHeckeSlashModularFormCharEnd_diagCosetGamma0_const: the scalar double coset acts by the expected scalar on modular forms.
• HeckeRing.GL2.twistedHeckeSlashCuspFormCharEnd_diagCosetGamma0_const: the corresponding statement for cusp forms.
• HeckeRing.GL2.heckeRingHomFunctionCharSpace_heckeTScalarGamma0: the scalar generator under the function-space Hecke-ring action.
• HeckeRing.GL2.heckeRingHomCharSpace_heckeTScalarGamma0: the scalar generator under the modular-form Hecke-ring action.
• HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTScalarGamma0: the cusp-form counterpart.

Provenance

The scalar-slash calculation is adapted from slash_diag_scalar in the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0), file LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08. The coset decomposition here instead uses Tau Ceti's normalizer API and its representative-independent right-coset sum.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.3 and §3.5.

theorem HeckeRing.GL2.twistedHeckeSlashSum_diagCosetGamma0_const {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) (f : UpperHalfPlane → ℂ) (hf : f ∈ functionCharSpace k χ) : twistedHeckeSlashSum k χ (diagCosetGamma0 N ![c, c] ⋯) f = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • f

The constant diagonal double coset acts on the function character space by χ(c) * c ^ (k - 2).

theorem HeckeRing.GL2.twistedHeckeSlashSumCharEnd_diagCosetGamma0_const {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) : twistedHeckeSlashSumCharEnd k χ (diagCosetGamma0 N ![c, c] ⋯) = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • 1

The constant diagonal double coset acts by χ(c) * c ^ (k - 2) as an endomorphism of the function character space.

theorem HeckeRing.GL2.twistedHeckeSlashModularFormCharEnd_diagCosetGamma0_const {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) : twistedHeckeSlashModularFormCharEnd k χ (diagCosetGamma0 N ![c, c] ⋯) = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • 1

The constant diagonal double coset acts on modular forms by χ(c) * c ^ (k - 2).

theorem HeckeRing.GL2.twistedHeckeSlashCuspFormCharEnd_diagCosetGamma0_const {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) : twistedHeckeSlashCuspFormCharEnd k χ (diagCosetGamma0 N ![c, c] ⋯) = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • 1

The constant diagonal double coset has the same scalar action on cusp forms.

theorem HeckeRing.GL2.heckeRingHomFunctionCharSpace_heckeTScalarGamma0 {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) : (heckeRingHomFunctionCharSpace k χ) (heckeTScalarGamma0 N c) = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • 1

The scalar Hecke generator acts on the function character space by χ(c) * c ^ (k - 2).

theorem HeckeRing.GL2.heckeRingHomCharSpace_heckeTScalarGamma0 {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) : (heckeRingHomCharSpace k χ) (heckeTScalarGamma0 N c) = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • 1

The scalar Hecke generator acts on modular forms by χ(c) * c ^ (k - 2).

theorem HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTScalarGamma0 {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (c : ℕ) (hc : 0 < c) (hcN : c.Coprime N) : (heckeRingHomCuspCharSpace k χ) (heckeTScalarGamma0 N c) = (↑(χ (ZMod.unitOfCoprime c hcN)) * ↑c ^ (k - 2)) • 1

The scalar Hecke generator acts on cusp forms by χ(c) * c ^ (k - 2).