The Hecke-ring action on nebentypus spaces #
The twisted slash operators give a right action, so composing the operators attached to D₁
and D₂ naturally produces the right-coset collision coefficient
m(D₂⁻¹, D₁⁻¹; D⁻¹). The multiplication of the Hecke ring instead uses
m(D₁, D₂; D). This file reconciles the two conventions using the Atkin–Lehner
anti-involution of Γ₀(N): composing it with inversion is an ambient automorphism preserving
Γ₀(N), and the Atkin–Lehner bar fixes every Γ₀(N) double coset.
The resulting basis identity extends by linearity to an anti-homomorphism. Since the Γ₀(N)
Hecke ring is commutative, this is a ring homomorphism. The construction is given first on the
function character space on which composition was proved, and then on the bundled modular-form
and cusp-form character spaces.
Main definitions #
HeckeRing.GL2.heckeRingHomFunctionCharSpace: the Hecke-ring action on twisted-invariant functions.HeckeRing.GL2.heckeRingHomCharSpace: the action on modular forms of nebentypusχ.HeckeRing.GL2.heckeRingHomCuspCharSpace: its restriction to cusp forms.
Main results #
HeckeRing.GL2.cuspToModFormCharSpace_twistedHeckeSlashCuspFormCharLinearMap: the inclusion of character spaces intertwines the two actions, so a statement aboutmodFormCharSpacespecialises tocuspFormCharSpace. This is the simp-normal form and carries@[simp]; consumers holding the ring-level operators normalise withheckeRingHomCuspCharSpace_applyandheckeRingHomCharSpace_applyfirst.
Provenance #
The final ring-homomorphism packaging is adapted from AINTLIB's
LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean, declaration
heckeRingHomCharSpace (Chris Birkbeck, Apache-2.0), at commit
2baa76f742bdb4fb8ee323fabba41203bd390e08. The convention bridge is new: AINTLIB proves its
composition formula directly with the Hecke-ring structure constants, while this repository's
right-coset composition theorem first exposes the reversed, inverted multiplicity.
The reversed, inverted multiplicity from a right slash action is the ordinary Γ₀(N)
Hecke-ring structure constant.
The linear extension of the twisted slash action is anti-multiplicative. This is the order
forced by a right action and multiplication by composition in Module.End.
The linear extension is multiplicative. Anti-multiplicativity becomes multiplicativity
because the Γ₀(N) Hecke ring is commutative.
The integral Γ₀(N) Hecke ring acts on the space of χ-invariant functions.
Equations
- HeckeRing.GL2.heckeRingHomFunctionCharSpace k χ = { toFun := ⇑(HeckeRing.GL2.twistedHeckeSlashRingCharLinearMap k χ), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The function-space Hecke action has the original linear extension as its underlying map.
The modular-form linear extension on a basis element.
On underlying functions, the modular-form extension is the function-space extension.
The modular-form extension is multiplicative.
The integral Γ₀(N) Hecke ring acts on modular forms of weight k and nebentypus χ.
Equations
- HeckeRing.GL2.heckeRingHomCharSpace k χ = { toFun := ⇑(HeckeRing.GL2.twistedHeckeSlashModularFormCharLinearMap k χ), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The modular-form Hecke action evaluates through its underlying linear extension.
The cusp-form linear extension on a basis element.
On underlying functions, the cusp-form extension is the function-space extension.
The cusp-form extension is multiplicative.
The integral Γ₀(N) Hecke ring acts on cusp forms of weight k and nebentypus χ.
Equations
- HeckeRing.GL2.heckeRingHomCuspCharSpace k χ = { toFun := ⇑(HeckeRing.GL2.twistedHeckeSlashCuspFormCharLinearMap k χ), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
The cusp-form Hecke action evaluates through its underlying linear extension.
The two Hecke actions agree on a cusp form. The action on S_k(N, χ) and the action on
M_k(N, χ) are built from the same twisted slash sums on functions, so the inclusion of
character spaces cuspToModFormCharSpace intertwines them. This is what lets a statement about
modFormCharSpace be specialised to cuspFormCharSpace.
Stated on the linear extensions rather than on heckeRingHom{,Cusp}CharSpace, because
heckeRingHomCuspCharSpace_apply and heckeRingHomCharSpace_apply are themselves simp lemmas:
this is the simp-normal form of the intertwining, and the ring-level statement is definitionally
this one.