The twisted slash sum descends to the nebentypus character spaces #
HeckeSlash/ModularForm.lean carries the unweighted slash sum from functions to
ModularForm and CuspForm, and bundles it as a Module.End ℂ. This file is the
nebentypus-twisted counterpart, and it lands on a different carrier.
Why the carrier is the character space #
The unweighted sum is invariant for the level it is taken at, so it acts on all of
ModularForm (G.map (mapGL ℝ)) k. The twisted sum is not: what is proved is that it preserves
the χ-eigenspace (twistedHeckeSlashSum_mem_functionCharSpace), which is what the weighting
buys. Whether that eigenspace is the largest subspace preserved is not established here and is
not needed. So the operators here are endomorphisms of
modFormCharSpace k χ and cuspFormCharSpace k χ, not of the ambient spaces, and the
underlying ModularForm is built only for a form already known to lie in the character space.
Invariance for Γ₁(N) is read off that same membership: a Γ₁(N) matrix lies in Γ₀(N) with
lower-right entry 1, so the character factor it contributes is χ 1 = 1 and the nebentypus
relation degenerates to plain invariance. Holomorphy is
mdifferentiable_twistedHeckeSlashSum, and the two cusp conditions are
isBoundedAt_twistedHeckeSlashSum and isZeroAt_twistedHeckeSlashSum. As in the untwisted
file the cusp-form case is derived from the modular-form one, adding only the vanishing
field, so neither invariance nor holomorphy is proved twice.
Main definitions #
HeckeRing.GL2.twistedHeckeSlashModularFormCharEnd: the twisted operator onmodFormCharSpace k χ.HeckeRing.GL2.twistedHeckeSlashCuspFormCharEnd: the twisted operator oncuspFormCharSpace k χ— the statement that the twisted action preserves cuspidality.
Main results #
HeckeRing.GL2.coe_twistedHeckeSlashModularFormCharEnd,HeckeRing.GL2.coe_twistedHeckeSlashCuspFormCharEnd: both aretwistedHeckeSlashSumon underlying functions.
Provenance #
Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0) at commit
2baa76f742bdb4fb8ee323fabba41203bd390e08, file
LeanModularForms/HeckeRIngs/GL2/Unified/NebentypusHeckeRingHom.lean lines 166-257, where the
same construction appears as nebentypusHeckeOpModularForm, nebentypusHeckeOp and
nebentypusHeckeOpLinear. The names here follow this repository's twistedHeckeSlashSum
prefix instead, the analytic inputs are the reusable statements of the two sibling modules
rather than inlined arguments, and the cusp-form operator is new.
References #
The twisted double coset as a ℂ-linear endomorphism of modFormCharSpace k χ. This is
the form the twisted Hecke operators are consumed in: bundling is what lets them compose and
later carry the ring structure of Nebentypus/CharRing.lean.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The twisted double coset as a ℂ-linear endomorphism of cuspFormCharSpace k χ — the
twisted action preserves cuspidality.
Equations
- HeckeRing.GL2.twistedHeckeSlashCuspFormCharEnd k χ D = { toFun := fun (f : ↥(cuspFormCharSpace k χ)) => ⟨HeckeRing.GL2.twistedHeckeSlashCuspForm✝ k χ D ↑f ⋯, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }
Instances For
The endomorphism is twistedHeckeSlashSum on underlying functions.
The cusp-form endomorphism is twistedHeckeSlashSum on underlying functions.
The twisted operator on modular forms is the weighted sum over any decomposition of the
double coset into right cosets: if the right cosets Γ₀(N) aᵢ are pairwise distinct and cover
the double coset, then the operator is
∑ᵢ delta0NebentypusChar N χ ⟨aᵢ, _⟩ • (f ∣[k] aᵢ).
The weight is not χ applied to aᵢ — aᵢ : GL (Fin 2) ℚ is not in the domain of χ. It is
delta0NebentypusChar, which reads χ off the upper-left unit of the Δ₀(N) witness that the
cover hypothesis supplies for aᵢ through mem_Delta0_of_cover.
So the operator is attached to the double coset, not to the representatives
twistedHeckeSlashSum happens to choose; the choice-independence itself is
twistedHeckeSlashSum_eq_sum_of_rightCosets (Nebentypus/Independence.lean). This is the twisted
counterpart of coe_heckeSlashModularFormEnd_eq_sum.
The twisted operator on cusp forms is the weighted sum over any decomposition of the double coset into right cosets, exactly as for modular forms.