The twisted slash sum extended over the Hecke ring, on the character space #

Nebentypus/Invariance.lean shows the twisted slash sum preserves functionCharSpace and restricts each double coset to twistedHeckeSlashSumCharEnd. This file takes the ℤ-linear extension of that assignment over the Hecke ring, exactly as Nebentypus/Ring.lean does for the unrestricted operator.

It is a separate module from Invariance.lean because the topic is different — that file is about preservation of the character space, this one is ring-level API — and it sits below Nebentypus/Composition.lean, which imports it in order to state the basis-element identity that consumes both this extension and its own composition theorem.

Two carriers, neither a specialisation of the other #

twistedHeckeSlashRingLinearMap (Nebentypus/Ring.lean) is the same Finsupp.linearCombination extension of the same per-coset assignment, valued in Module.End ℂ (ℍ → ℂ). The two are not interchangeable: the composition results of Nebentypus/Composition.lean hold only on the character space, so the carrier is what distinguishes them and neither restricts to the other by a general principle.

Main definitions #

HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap: the ℤ-linear extension of twistedHeckeSlashSumCharEnd over 𝕋 Δ₀(N) Γ₀(N) ℤ, valued in Module.End ℂ (functionCharSpace k χ).

Main results #

HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap_apply: evaluation as a finite sum.
HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap_single: the value on a basis element is the scaled twisted operator of that double coset. With map_zero/map_add this determines the map.

Provenance #

Adapted from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/Unified/TwistedHeckeRing.lean, Chris Birkbeck, Apache-2.0, https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08), whose twistedHeckeSumFunction (line 842) is the extension below. The source states it over its own gamma0TwistedInvariantFunctionSubmodule; this repository's name for that carrier is functionCharSpace, and the double-coset indexing and the HeckeCosetModule.single spelling are this repository's, not the source's. The statement shape follows main's own untwisted heckeSlashGamma1RingModularFormLinearMap (HeckeSlash/Ring.lean).

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.

source

noncomputable def HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap {N : ℕ} (k : ℤ) (χ : (ZMod N)ˣ →* ℂ ˣ) [NeZero N] :

HeckeRing (Delta0 N) (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℚ) (CongruenceSubgroup.Gamma0 N)) ℤ →ₗ[ℤ ] Module.End ℂ ↥(functionCharSpace k χ)

The ℤ-linear extension of twistedHeckeSlashSumCharEnd to formal ℤ-combinations of double cosets of Γ₀(N), on the carrier the twisted sum preserves.

twistedHeckeSlashRingLinearMap (Nebentypus/Ring.lean) is the same extension on all of ℍ → ℂ. The two are not interchangeable: the composition results of Nebentypus/Composition.lean are available only on the character space, so the carrier is what distinguishes them, and neither is a specialisation of the other.

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

Equations