Cusp forms descend through the level-raising operator #
Degeneracy.lean has a Descent section, which answers the question the conductor theorem asks:
given only that the level-raise V_d f is a form, what can be said about f itself? Two of the
three conditions a form must satisfy are answered there — the transformation law by
slash_conjScale_eq_smul_of_slash_scaleGL, and holomorphy by
mdifferentiable_of_comp_scaleGL_smul. The third, vanishing at the cusps, is not: the whole file
mentions IsCusp once. This file supplies that missing third member, and then closes the loop:
with all three conditions in hand, f itself bundles into a CuspForm of the lowered level
Γ₁(N / l).
The one geometric input #
Everything rests on the fact that diag(d, 1)⁻¹ · A carries ∞ to a cusp, for any
A ∈ SL(2, ℤ). That is not a computation: the matrix is rational, and rational matrices carry
cusps to cusps — IsCusp.smul_map_ratCast, already in Cusps/Rat/Basic.lean. Degeneracy.lean
supplies scaleGLRat d, the matrix diag(d, 1) over ℚ, and its pushforward to scaleGL d.
Main results #
TauCeti.isCusp_inv_scaleGL_mul_mapGL_smul_infty:diag(d, 1)⁻¹ · Asends∞to a cusp of any arithmetic subgroup.TauCeti.isZeroAtImInfty_slash_inv_scaleGL_mul_mapGL: a cusp form therefore vanishes ati∞after slashing bydiag(d, 1)⁻¹ · A.TauCeti.isZeroAt_of_smul_slash_scaleGL_eq: vanishing at the cusps descends — if the level-raise offis a cusp form for any arithmetic subgroup, thenfvanishes at every cusp of any arithmetic subgroup.TauCeti.nebentypus_slash_scaleGL_of_mem_cuspFormCharSpace: the nebentypus relation of the level-raise, read offf ∣[k] diag(l, 1)with the normalizing scalar cancelled.TauCeti.cuspFormOfSmulSlashScaleGL,TauCeti.coe_cuspFormOfSmulSlashScaleGL: the descent bundle —fas a cusp form of levelΓ₁(N / l), and its underlying function.
Provenance #
Adapted from the AINTLIB LeanModularForms project
(LeanModularForms/Eigenforms/ConductorTheorem.lean, Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08), lines
354–486 and 500–541, whose zero_at_cusps_of_levelRaiseFun_eq (:471) and
conductorTheoremCaseA_cuspForm (:511) are the two theorems this file is built around.
Statements only, and four of the first window's nine declarations are not reproduced at all:
cuspWitnessLevelRaiseInv(:354), its private helpercuspWitnessLevelRaiseInv_first_col(:360) andgcd_levelRaise_first_col_ne_zerobuild an explicitSL(2, ℤ)witness byClassical.chooseoverIsCoprime.exists_SL2_col, because the source proves the cusp condition through mathlib'sisCusp_SL2Z_iff'(theSL(2, ℤ)-orbit criterion). Mathlib also offersisCusp_SL2Z_iff, which says the cusps ofSL(2, ℤ)are exactlyℙ¹(ℚ), andisCusp_SL2Z_iff'is derived from it by manufacturing that witness internally. Routing through rationality instead —IsCusp.smul_map_ratCast— discharges the cusp condition with no witness, noClassical.choose, and no gcd arithmetic.isZeroAtImInfty_slash_iff_levelRaiseFun_eq(:425) is one rewrite of what this repository already has asslash_scaleGL_slash_mapGL, so it is inlined rather than named.
Of the second window's three declarations, one is likewise not reproduced:
cuspFormToModularForm_mem_modFormCharSpace_iff_mem_cuspFormCharSpace(:500) moves the character-space hypothesis from the cusp form to its underlying modular form, because the source's transformation law is stated for aModularForm. This repository'sslash_mapGL_eq_self_of_mem_Gamma1_divasks instead for the nebentypus relation of the bare function, so the bridge is not a coercion but a scalar cancellation, and it isnebentypus_slash_scaleGL_of_mem_cuspFormCharSpacebelow.
The source is phrased over its own levelRaiseFun and levelRaiseMatrix, neither of which exists
here; the statements below use scaleGL and the hypothesis shape
⇑g = d ^ (1 - k) • (f ∣[k] scaleGL d) that smul_slash_scaleGL_eq was written to be rewritten
with. The source also carries its character as a DirichletCharacter ℂ N and phrases Case A over
χ.FactorsThrough (N / l); here the character is the units homomorphism (ZMod N)ˣ →* ℂˣ that
cuspFormCharSpace is indexed by, and the descent hypothesis is triviality on the kernel of
ZMod.unitsMap, which is the form slash_mapGL_eq_self_of_mem_Gamma1_div already takes.
References #
- Miyake, Modular forms, Theorem 4.6.4.
diag(d, 1)⁻¹ · A carries ∞ to a cusp. For any A ∈ SL(2, ℤ) and any arithmetic
subgroup, the point (diag(d, 1)⁻¹ · A) • ∞ is a cusp.
The matrix is rational, and that is the whole proof: IsCusp.smul_map_ratCast carries the cusp
∞ along it. The source instead exhibits an explicit SL(2, ℤ) matrix with the same first
column; nothing here needs one.
A cusp form vanishes at i∞ after slashing by diag(d, 1)⁻¹ · A, because that matrix sends
∞ to a cusp and CuspFormClass.zero_at_cusps covers every cusp.
Nothing here is specific to a level: the cusp condition above holds for any arithmetic subgroup,
and zero_at_cusps asks only that g be a cusp form for the same one. Stated over
CuspFormClass so it applies to CuspForm and to anything else carrying that class.
Vanishing at the cusps descends through V_d. If the level-raise of f is a cusp form —
for any arithmetic subgroup — then f vanishes at every cusp of any arithmetic subgroup.
The two subgroups are independent and neither is a level of f: Γ' is where g is a cusp form,
and Γ is where the cusp c lives. f itself is only a function, which is the situation the
conductor theorem is in.
With the transformation law (slash_conjScale_eq_smul_of_slash_scaleGL) and holomorphy
(mdifferentiable_of_comp_scaleGL_smul) of Degeneracy.lean's Descent section, this is the
third and last condition needed to exhibit f as a cusp form of the lower level.
The descent bundle #
The nebentypus relation descends to the level-raised function. If a cusp form g of level
N lies in the χ-eigenspace and is the level-raise of f, then f ∣[k] diag(l, 1) satisfies
the classical nebentypus relation for χ on the nose.
This is the hypothesis slash_mapGL_eq_self_of_mem_Gamma1_div asks for.
The conductor descent, bundled. If the level-raise of f is a cusp form g of level N
whose nebentypus χ is trivial on the kernel of (ZMod N)ˣ → (ZMod (N / l))ˣ, and if f is
T-periodic, then f is itself a cusp form of the lowered level Γ₁(N / l).
Equations
- TauCeti.cuspFormOfSmulSlashScaleGL l N hlN k χ hχ f g hgχ hg hT = { toFun := f, slash_action_eq' := ⋯, holo' := ⋯, zero_at_cusps' := ⋯ }
Instances For
The bundled cuspFormOfSmulSlashScaleGL has underlying function f.