The twisted operator of diag(1, p) is the classical Tₚ on M_k(N, χ) and S_k(N, χ)

The Γ₀(N) Hecke ring acts on the nebentypus spaces M_k(N, χ) and S_k(N, χ) through the χ-twisted slash sums (HeckeSlash/Nebentypus/*), while the classical Tₚ on M_k(Γ₁(N)) and S_k(Γ₁(N)) is the untwisted sum over Γ₁(N) cosets (HeckeSlash/Prime.lean). This file identifies the two at every prime p: on the nebentypus spaces the twisted operator of the generator diag(1, p) is the classical Tₚ.

Why the twist disappears

At a prime p ∤ N, the Γ₀(N) right cosets of diag(1, p) are named by the same p + 1 representatives as over Γ₁(N) (Gamma0/Diagonal/PrimeCosets.lean): !![1, j; 0, p] and σ · diag(p, 1) with σ ∈ Γ₀(N) of bottom row (N, p). The twisting character reads the upper-left unit of a representative: it is 1 on the upper-triangular ones, and on σ · diag(p, 1) it is χ(σ₀₀ p), which is 1 because σ₀₀ p ≡ 1 (mod N) by the determinant (Delta0UpperUnit_upperTriRep, Delta0UpperUnit_mapGL_mul_scaleRep). So every weight is 1, and the only character that survives is the nebentypus factor χ(p) produced by slashing f by σ — exactly the factor the classical formula carries on the Γ₁(N) side. At a prime p ∣ N there are only the p upper-triangular representatives, all of weight 1, and both operators are the upper-triangular Uₚ.

The computation happens once, on functions with the nebentypus χ (twistedHeckeSlashSum_diagCosetGamma0_of_prime, …_of_dvd); the modular-form and cusp-form statements read it through the coercions to functions.

Main results

• HeckeRing.GL2.twistedHeckeSlashSum_diagCosetGamma0_of_prime, HeckeRing.GL2.twistedHeckeSlashSum_diagCosetGamma0_of_dvd: on a function with nebentypus χ, the twisted slash sum of diag(1, p) is the classical Tₚ formula.
• HeckeRing.GL2.coe_twistedHeckeSlashModularFormCharEnd_diagCosetGamma0 and HeckeRing.GL2.coe_twistedHeckeSlashCuspFormCharEnd_diagCosetGamma0: at every prime p, the twisted operator of diagCosetGamma0 N ![1, p] is heckeTNat k p, resp. heckeTCuspNat k p, as functions on ℍ.
• HeckeRing.GL2.heckeTNat_mem_modFormCharSpace and HeckeRing.GL2.heckeTCuspNat_mem_cuspFormCharSpace: the classical Tₚ preserves the nebentypus spaces.
• HeckeRing.GL2.heckeRingHomCharSpace_heckeTGeneratorGamma0 and HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTGeneratorGamma0: the Hecke-ring action of the generator heckeTGeneratorGamma0 N p on M_k(N, χ), resp. S_k(N, χ), is the classical operator restricted to the space, as an equality of endomorphisms; the coe_… companions read the same identity on a single form.

Scope

This file treats prime indices only.

Provenance

The prime case of heckeRingHomCharSpace_D_p_eq_scalar_charRestrict of the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms). In the source the twist runs the other way, so its statement carries a factor χ(p)⁻¹; with this repository's convention (Nebentypus/Basic.lean, "Which way the character goes") the factor is 1 and the identification is exact.

theorem HeckeRing.GL2.twistedHeckeSlashSum_diagCosetGamma0_of_prime {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) (h : p.Coprime N) {F : UpperHalfPlane → ℂ} (hF : F ∈ functionCharSpace k χ) : twistedHeckeSlashSum k χ (diagCosetGamma0 N ![1, p] ⋯) F = heckeSlashUpperTri k p F + ↑(χ (ZMod.unitOfCoprime p h)) • SlashAction.map k (scaleRep p) F

The twisted slash sum of diag(1, p) at a prime p ∤ N, on a function with nebentypus χ: Uₚ f + χ(p) • (f ∣[k] diag(p, 1)), the classical Tₚ formula.

theorem HeckeRing.GL2.twistedHeckeSlashSum_diagCosetGamma0_of_dvd {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) (hpN : p ∣ N) {F : UpperHalfPlane → ℂ} (hF : F ∈ functionCharSpace k χ) : twistedHeckeSlashSum k χ (diagCosetGamma0 N ![1, p] ⋯) F = heckeSlashUpperTri k p F

The twisted slash sum of diag(1, p) at a prime p ∣ N, on a function with nebentypus χ: the upper-triangular operator Uₚ.

theorem HeckeRing.GL2.coe_twistedHeckeSlashModularFormCharEnd_diagCosetGamma0 {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) (f : ↥(modFormCharSpace k χ)) : ⇑↑((twistedHeckeSlashModularFormCharEnd k χ (diagCosetGamma0 N ![1, p] ⋯)) f) = ⇑((heckeTNat k p) ↑f)

At every prime, the twisted operator of diag(1, p) on M_k(N, χ) is the classical Tₚ, as functions on ℍ: Uₚ f + χ(p) • (f ∣[k] diag(p, 1)) when p ∤ N, and Uₚ f when p ∣ N.

theorem HeckeRing.GL2.coe_twistedHeckeSlashCuspFormCharEnd_diagCosetGamma0 {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) (f : ↥(cuspFormCharSpace k χ)) : ⇑↑((twistedHeckeSlashCuspFormCharEnd k χ (diagCosetGamma0 N ![1, p] ⋯)) f) = ⇑((heckeTCuspNat k p) ↑f)

At every prime, the twisted operator of diag(1, p) on S_k(N, χ) is the classical Tₚ, as functions on ℍ: Uₚ f + χ(p) • (f ∣[k] diag(p, 1)) when p ∤ N, and Uₚ f when p ∣ N.

theorem HeckeRing.GL2.coe_heckeRingHomCharSpace_heckeTGeneratorGamma0 {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) (f : ↥(modFormCharSpace k χ)) : ↑(((heckeRingHomCharSpace k χ) (heckeTGeneratorGamma0 N p)) f) = (heckeTNat k p) ↑f

The Hecke-ring generator at a prime acts on M_k(N, χ) as the classical Tₚ, on each form.

theorem HeckeRing.GL2.coe_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0 {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) (f : ↥(cuspFormCharSpace k χ)) : ↑(((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) f) = (heckeTCuspNat k p) ↑f

The Hecke-ring generator at a prime acts on S_k(N, χ) as the classical Tₚ, on each form.

theorem HeckeRing.GL2.heckeTNat_mem_modFormCharSpace {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ modFormCharSpace k χ) : (heckeTNat k p) f ∈ modFormCharSpace k χ

The classical Tₚ preserves M_k(N, χ): it agrees there with the Hecke-ring action.

theorem HeckeRing.GL2.heckeTCuspNat_mem_cuspFormCharSpace {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) : (heckeTCuspNat k p) f ∈ cuspFormCharSpace k χ

The classical Tₚ preserves S_k(N, χ): it agrees there with the Hecke-ring action.

theorem HeckeRing.GL2.heckeRingHomCharSpace_heckeTGeneratorGamma0 {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) : (heckeRingHomCharSpace k χ) (heckeTGeneratorGamma0 N p) = LinearMap.restrict (heckeTNat k p) ⋯

The Hecke-ring generator at a prime acts on M_k(N, χ) as the classical Tₚ, as an equality of endomorphisms of the space.

theorem HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTGeneratorGamma0 {N p : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) [NeZero N] (hp : Nat.Prime p) : (heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p) = LinearMap.restrict (heckeTCuspNat k p) ⋯

The Hecke-ring generator at a prime acts on S_k(N, χ) as the classical Tₚ, as an equality of endomorphisms of the space.