The level-raising degeneracy maps V_d #
For a positive integer d, the level-raising (or degeneracy) map V_d sends a function on
the upper half-plane to τ ↦ f (d τ). It is the slash action by diag(d, 1), renormalized by
d ^ (1 - k) so that no power of d is introduced.
Properties of f transport up to V_d f — the level of the congruence subgroup, the
eigenvalue and nebentypus transport, the q-expansion — which is what makes V_d a map of
modular forms. Two of them also read back down: the slash transformation law
(slash_conjScale_eq_smul_of_slash_scaleGL) and holomorphy
(mdifferentiable_of_comp_scaleGL_smul), which is what recognizes a bare function as a form at
the lower level. The q-expansion results go up only.
Main definitions #
TauCeti.scaleGL d: the diagonal element!![d, 0; 0, 1]ofGL(2, ℝ), a value ofTauCeti.diagGL.TauCeti.scaleGLRat d: the same diagonal element overℚ.TauCeti.conjScale: its conjugation action on an integral matrix whose lower-left entry is divisible byd,(a, b; d c, e) ↦ (a, d b; c, e).TauCeti.ModularForm.levelRaise,TauCeti.CuspForm.levelRaise: the operatorV_d, taking a form for𝒢to a form for any group𝒢'conjugated into𝒢bydiag(d, 1), together with theirℂ-linear packagingslevelRaiseₗ.
Main results #
TauCeti.map_ratCast_scaleGLRat: the rational scaling matrix pushes forward toscaleGL d.TauCeti.ModularForm.levelRaise_apply:(V_d f) τ = f (d τ), the defining formula from which the algebraic properties (levelRaise_one_apply,ModularForm.levelRaise_one,levelRaise_levelRaise,levelRaise_injective) all follow byext.TauCeti.slash_mapGL_eq_smul_of_unitsMap_eq: a function whose level-raise carries a nebentypus trivial on the kernel of(ZMod N)ˣ → (ZMod (N/l))ˣtransforms under eachγ' ∈ Γ₀(N / l)by the character value at any unit lying over the label ofγ'.TauCeti.slash_mapGL_eq_self_of_mem_Gamma1_div: the trivial-label case of the previous result — such a function is invariant under all ofΓ₁(N / l).TauCeti.Gamma1_map_le_conjAct_scaleGL,TauCeti.Gamma0_map_le_conjAct_scaleGL: the level transport,Γ₁(dM) ≤ diag(d,1)⁻¹ Γ₁(M) diag(d,1)and likewise forΓ₀, which is what makesV_da mapM_k(Γ₁(M)) → M_k(Γ₁(dM)).TauCeti.exists_eq_T_zpow_mul_conjScale_mul_T_zpow: theT-factorisation, in the other direction. Forl ∣ N, everyγ' ∈ Γ₀(N / l)isT ^ i * conjScale l γ c * T ^ jfor somei, j, c : ℤand someγ ∈ Γ₀(N)whose lower-left entry factors asγ 1 0 = l * c— a level can be raised back fromN / ltoNat the cost of two translations — together with the bookkeepingγ 1 1 = γ' 1 1 - γ' 1 0 * jthat pins the lower-right entry ofγ, which is what a nebentypus of levelNreads off it.TauCeti.ModularForm.slash_levelRaise_eq_smul,TauCeti.CuspForm.slash_levelRaise_eq_smul: the eigenvalue transport. SlashingV_d fbyγproduces the same scalar that slashingfby the conjugate matrixconjScale d γdoes.TauCeti.CuspForm.diamondOpCusp_levelRaise:V_dintertwines diamond operators between a divisor level and any multiple of the raised level.TauCeti.ModularForm.levelRaise_mem_modFormCharSpace_of_dvd,TauCeti.CuspForm.levelRaise_mem_cuspFormCharSpace_of_dvd: the nebentypus transport, stated at every levelNwithd * M ∣ N. Since thediag(d, 1)-conjugate of aΓ₀(N)matrix lies inΓ₀(M)with the same lower-right entry,V_dcarriesM_k(Γ₁(M), χ)intoM_k(Γ₁(N), χ ∘ ZMod.unitsMap), and likewise forS_k: the nebentypus ofV_d fis that offread along(ZMod N)ˣ → (ZMod M)ˣ.TauCeti.ModularForm.levelRaise_mem_modFormCharSpace,TauCeti.CuspForm.levelRaise_mem_cuspFormCharSpace: theN = d * Mcase, the transport to exactly the raised level.TauCeti.ModularForm.ofLe_mem_modFormCharSpace,TauCeti.CuspForm.ofLe_mem_cuspFormCharSpace: the same transport for the degeneracy mapV₁at a divisor. Reading a form of levelMas a form of levelNfor anyM ∣ NcarriesM_k(Γ₁(M), χ)intoM_k(Γ₁(N), χ ∘ ZMod.unitsMap), and likewise forS_k. These are thed = 1case of the two theorems above, restated for the subgroup inclusionofLe; the restatement is exactlyModularForm.levelRaise_oneandCuspForm.levelRaise_one, so no nebentypus argument is repeated for them.TauCeti.slash_conjScale_eq_smul_of_slash_scaleGL,TauCeti.mdifferentiable_of_comp_scaleGL_smul: the descent, for anf : ℍ → ℂnot assumed to be a form. If the level-raise offis an eigenvector of the slash byγ, thenfis one forconjScale d γwith the same eigenvalue, and if the level-raise offis holomorphic then so isf. These are what read a transformation law and holomorphy back down fromV_d ftof, as the level-lowering step of the conductor theorem does.TauCeti.ModularForm.qExpansion_levelRaise,TauCeti.CuspForm.qExpansion_levelRaise: theq-expansion ofV_d fis that offwithqreplaced byq ^ d, that is, itsPowerSeries.expand d; on coefficients (TauCeti.ModularForm.qExpansion_levelRaise_coeffandTauCeti.CuspForm.qExpansion_levelRaise_coeff),aₙ(V_d f) = a_{n/d}(f)ford ∣ nand0otherwise.ModularForm.isSupportedOnDvd_qExpansion_levelRaise,CuspForm.isSupportedOnDvd_qExpansion_levelRaise: the same fact as a support statement — theq-expansion ofV_d fis supported on the multiples ofd. This is the forward half of the Atkin–Lehner description of the old subspace.
The old subspace of Layer 3 of the ModularForms roadmap is spanned by the images of the V_d,
and the conductor statement of Layer 4 is phrased with this normalization of V_d.
References #
- Diamond–Shurman, A first course in modular forms, §5.6
- Miyake, Modular forms, §4.6
- The
T-factorisation section is ported from the AINTLIBLeanModularFormsproject (Chris Birkbeck),HeckeRIngs/GL2/LevelRaise.lean, declarationsexists_T_levelRaiseConj_T_factor(:491) and its supportseq_T_zpow_mul_levelRaiseConj_mul_T_zpow(:471),primeProductCoprime(:410),dvd_primeProductCoprime_of_not_dvd(:413),not_dvd_primeProductCoprime_of_dvd(:419),exists_shift_isCoprime(:430),shiftJ(:450),shiftJ_spec(:453) andnatCast_dvd_levelRaiseConj_lower_left(:465), all Apache-2.0 at commit2baa76f742bdb4fb8ee323fabba41203bd390e08. The source'slevelRaiseConjOfDvd(:98) is this file'sconjScale, so the statement is phrased withconjScaleand TauCeti'sGamma0API rather than porting a second conjugation; the source'sshiftJ/shiftJ_specpair is not ported at all, its Bézout step being TauCeti's existingZMod.exists_dvd_sub_val_mul. - The descent section adapts AINTLIB commit
2baa76f74, Apache-2.0, Chris Birkbeck,projects/LeanModularForms/LeanModularForms/Eigenforms/ConductorTheorem.leanlines 84-137 — the level-lowering block ofconductor_theorem_dichotomy_cuspForm_strong. Half of that block is deliberately not ported:ModularGroup_T_mem_Gamma1,conductor_slash_levelRaise_eqandsmul_levelRaiseFunalready exist here in more general form (T_zpow_mem_Gamma1,ModularForm.slash_levelRaise_eq_smulwithmem_modFormCharSpace_iff_nebentypus, and theℂ-linearity oflevelRaiseₗ), and AINTLIB's twofun_eq_..._inv_smullemmas are not needed, mathlib'smdifferentiable_smulreaching the holomorphy descent directly. ModularForm.isSupportedOnDvd_qExpansion_levelRaiseand its cusp-form counterpart are adapted from AINTLIB commit2baa76f74, Apache-2.0, Chris Birkbeck,projects/LeanModularForms/LeanModularForms/Eigenforms/AtkinLehner.lean, where they areqExpansion_modularFormLevelRaise_isSupportedOnDvdandqExpansion_levelRaise_isSupportedOnDvd. They live here rather than beside the rest of that file's material because they are statements aboutV_d; the power-series predicate they conclude in isPowerSeries.IsSupportedOnDvd, adapted from the same source file intoTauCeti/RingTheory/PowerSeries/Support.lean. Each proof is one rewrite byqExpansion_levelRaiseand thenPowerSeries.isSupportedOnDvd_expand, where the source recomputes coefficients.
The scaling matrix diag(d, 1) #
The diagonal element !![d, 0; 0, 1] of GL(2, ℝ), for d a nonzero natural number.
Slashing by it is, up to the normalizing scalar d ^ (1 - k), the level-raising operator
V_d.
Equations
- TauCeti.scaleGL d = TauCeti.diagGL ![Units.mk0 ↑d ⋯, 1]
Instances For
diag(d, 1) over ℚ. scaleGL is stated over ℝ, where the slash action lives, but the
cusp argument needs the same matrix over ℚ, because what makes diag(d, 1)⁻¹ · A carry cusps to
cusps is precisely that it is rational.
Equations
- TauCeti.scaleGLRat d = TauCeti.diagGL ![Units.mk0 ↑d ⋯, 1]
Instances For
scaleGLRat pushes forward to scaleGL.
Scaling down divides the argument.
Slashing by diag(d, 1) rescales the argument and introduces the factor d ^ (k - 1).
The defining formula for V_d, for a bare function: the renormalized slash
d ^ (1 - k) • (f ∣[k] diag(d, 1)) is τ ↦ f (d τ), with no stray power of d. This is
ModularForm.levelRaise_apply for an f : ℍ → ℂ that is not yet known to be a modular form,
which is the situation of the conductor theorem: there the transformation law of f is what is
being proved, so f cannot be assumed to carry one.
Stated between functions rather than pointwise, because that is the form in which a hypothesis
⇑g = d ^ (1 - k) • (f ∣[k] diag(d, 1)) is rewritten; congrFun gives the values. It is not a
simp lemma: Pi.smul_apply takes the pointwise left-hand side out of simp-normal form.
The level-raising operator #
The conjugation conditions compose: if 𝒢'' is conjugated into 𝒢' by diag(d,1) and
𝒢' into 𝒢 by diag(e,1), then 𝒢'' is conjugated into 𝒢 by diag(de,1).
At d = 1 the conjugation condition is the subgroup inclusion: diag(1, 1) is the
identity, so 𝒢' ≤ diag(1, 1)⁻¹ 𝒢 diag(1, 1) says no more than 𝒢' ≤ 𝒢. This is what lets
levelRaise_one name its ofLe without carrying a second inclusion hypothesis.
The level-raising (degeneracy) operator V_d, (V_d f) τ = f (d τ), as a map from modular
forms for 𝒢 to modular forms for a group 𝒢' conjugated into 𝒢 by diag(d, 1).
Equations
- TauCeti.ModularForm.levelRaise d h f = ↑d ^ (1 - k) • ModularForm.ofLe h (ModularForm.translate f (TauCeti.scaleGL d))
Instances For
The defining formula for V_d: (V_d f) τ = f (d τ), with no stray power of d.
The algebraic properties of V_d all follow from this by ext.
The level-raising operator, as a ℂ-linear map.
Equations
- TauCeti.ModularForm.levelRaiseₗ d h = { toFun := TauCeti.ModularForm.levelRaise d h, map_add' := ⋯, map_smul' := ⋯ }
Instances For
V_d is injective: f (d τ) determines f, since τ ↦ d τ is a bijection of ℍ.
V_d is injective as a ℂ-linear map, so its range is a copy of M_k(𝒢) inside
M_k(𝒢').
V₁ is the restriction map: it changes nothing but the invariance group.
V₁ is the restriction map, as forms. The pointwise statement of
TauCeti.ModularForm.levelRaise_one_apply, packaged as an equality of modular forms: at d = 1
the level-raising operator is ofLe. This is what lets a statement about V_d be specialised
to one about restriction along 𝒢' ≤ 𝒢, rather than reproved for it.
It is stated in the root ModularForm namespace, beside ModularForm.ofLe, so that dot
notation on a ModularForm resolves.
V₁ at an unchanged level is the identity. When the invariance group stays 𝒢, the
level-raising operator at d = 1 fixes every modular form.
The level-raising operators compose: V_d ∘ V_e = V_{de}.
The level-raising (degeneracy) operator V_d on cusp forms, (V_d f) τ = f (d τ).
Equations
- TauCeti.CuspForm.levelRaise d h f = ↑d ^ (1 - k) • CuspForm.ofLe h (CuspForm.translate f (TauCeti.scaleGL d))
Instances For
The defining formula for V_d on cusp forms: (V_d f) τ = f (d τ), with no stray
power of d.
The level-raising operator on cusp forms, as a ℂ-linear map.
Equations
- TauCeti.CuspForm.levelRaiseₗ d h = { toFun := TauCeti.CuspForm.levelRaise d h, map_add' := ⋯, map_smul' := ⋯ }
Instances For
V_d is injective on cusp forms: f (d τ) determines f, since τ ↦ d τ is a bijection
of ℍ.
V_d is injective as a ℂ-linear map on cusp forms, so its range is a copy of S_k(𝒢)
inside S_k(𝒢'). These ranges are what span the old subspace.
V₁ is the restriction map: it changes nothing but the invariance group.
V₁ is the restriction map, as forms. The pointwise statement of
TauCeti.CuspForm.levelRaise_one_apply, packaged as an equality of cusp forms: at d = 1 the
level-raising operator is ofLe. This is what lets a statement about V_d be specialised to
one about restriction along 𝒢' ≤ 𝒢, rather than reproved for it.
It is stated in the root CuspForm namespace, beside CuspForm.ofLe, so that dot notation
on a CuspForm resolves.
V₁ at an unchanged level is the identity. When the invariance group stays 𝒢, the
level-raising operator at d = 1 fixes every cusp form.
The level-raising operators compose: V_d ∘ V_e = V_{de}.
Level transport for the congruence subgroups #
The diag(d, 1)-conjugate of an integral matrix whose lower-left entry is d * c: the
entries are rearranged as (a, b; d c, e) ↦ (a, d b; c, e), which is again integral of
determinant one.
Equations
- TauCeti.conjScale d γ c hc = ⟨!![↑γ 0 0, ↑d * ↑γ 0 1; c, ↑γ 1 1], ⋯⟩
Instances For
Conjugation by diag(d, 1) realizes conjScale.
The diag(d, 1)-conjugate of a matrix γ ∈ Γ₀(N) lies in Γ₀(M) whenever d * M ∣ N, and
the conjugation leaves the lower-right entry alone: the diamond label of γ is read along the
reduction (ZMod N)ˣ → (ZMod M)ˣ.
Level transport for Γ₁: conjugation by diag(d, 1) carries Γ₁(dM) into Γ₁(M).
This is what makes V_d a map M_k(Γ₁(M)) → M_k(Γ₁(dM)).
Level transport at a divisor. Whenever d * M ∣ N, conjugation by diag(d, 1) carries
Γ₁(N) into Γ₁(M): this is what makes V_d a map S_k(Γ₁(M)) → S_k(Γ₁(N)), not only for
N = d * M but for every multiple of it.
Level transport for Γ₀: conjugation by diag(d, 1) carries Γ₀(dM) into Γ₀(M).
This is what makes V_d a map M_k(Γ₀(M)) → M_k(Γ₀(dM)).
Level transport for Γ₀ at a divisor. Whenever d * M ∣ N, conjugation by
diag(d, 1) carries Γ₀(N) into Γ₀(M): this is what makes V_d a map
S_k(Γ₀(M)) → S_k(Γ₀(N)) for every multiple N of d * M.
The T-factorisation of Γ₀(N / l) #
The T-factorisation of Γ₀(N / l). For l ∣ N, every γ' ∈ Γ₀(N / l) is a product
T ^ i * conjScale l γ c * T ^ j for some i, j, c : ℤ and some γ ∈ Γ₀(N) whose lower-left
entry factors as γ 1 0 = l * c: the level of γ' can be raised back from N / l to N at the
cost of two translations. Since conjScale and the translations all fix the lower-right entry up
to the recorded shift, the last conjunct γ 1 1 = γ' 1 1 - γ' 1 0 * j pins the lower-right entry
of γ, which is what a nebentypus of level N reads off it.
Slashing a level-raise, and the transport of the nebentypus #
Slashing by diag(d, 1) and then by an integral matrix γ whose lower-left entry is
divisible by d is slashing by the conjugate matrix conjScale d γ and then by diag(d, 1).
Slashing a level-raise by an integral matrix γ whose lower-left entry is divisible by d
is the level-raise of the slash of f by the conjugate matrix conjScale d γ.
Slashing a level-raised cusp form by an integral matrix γ whose lower-left entry is
divisible by d is the level-raise of the slash of f by the conjugate matrix
conjScale d γ.
Eigenvalue transport. If f is an eigenvector of the slash by conjScale d γ with
eigenvalue z, then V_d f is an eigenvector of the slash by γ with the same eigenvalue.
Applied to γ ∈ Γ₀(dM) this is what transports the nebentypus, in
levelRaise_mem_modFormCharSpace.
Eigenvalue transport (cusp forms). If f is an eigenvector of the slash by
conjScale d γ with eigenvalue z, then V_d f is an eigenvector of the slash by γ with
the same eigenvalue.
Descending along the level-raise #
Eigenvalue descent, the converse of ModularForm.slash_levelRaise_eq_smul. If the
level-raise of f is an eigenvector of the slash by γ with eigenvalue z, then f itself is
an eigenvector of the slash by the conjugate matrix conjScale d γ, with the same eigenvalue.
Both sides of the hypothesis and of the conclusion scale together, so the normalizing scalar
d ^ (1 - k) of V_d cancels and does not appear. Applied to γ ∈ Γ₀(dM), this is what
descends a nebentypus through V_d: the level-lowering step of the conductor theorem, where
f is only known to be a function and this transformation law is what exhibits it as a form.
Holomorphy descent. If τ ↦ f (d τ) is holomorphic on ℍ, then so is f. This is
UpperHalfPlane.mdifferentiable_comp_smul_iff — holomorphy is invariant under any
positive-determinant Möbius action — read at g = diag(d, 1); with smul_slash_scaleGL_eq it
descends holomorphy through V_d at every weight.
The nebentypus character of a level-raise #
V_d intertwines the diamond operators. For d * M ∣ N, the diamond operator ⟨u⟩ of
level N acts on a level-raised form V_d f as the diamond operator of level M at the
reduction of u acts on f. Both sides are slashes by a matrix of Γ₀, related by the
diag(d, 1)-conjugation, which preserves the lower-right entry.
The nebentypus of a level-raise. For d * M ∣ N, V_d carries M_k(Γ₁(M), χ) into
M_k(Γ₁(N), χ ∘ (ZMod N)ˣ → (ZMod M)ˣ): the character of V_d f at level N is the character
of f read along the reduction map. The target level is any multiple of d * M.
The nebentypus of a level-raise at the exact level. The N = d * M case of
TauCeti.ModularForm.levelRaise_mem_modFormCharSpace_of_dvd.
The nebentypus of a level-raise (cusp forms). For d * M ∣ N, V_d carries
S_k(Γ₁(M), χ) into S_k(Γ₁(N), χ ∘ (ZMod N)ˣ → (ZMod M)ˣ): the character of V_d f at level
N is the character of f read along the reduction map.
This is the character half only. That V_d f is old is the separate statement
TauCeti.levelRaise_mem_cuspFormsOld, which additionally needs M ≠ N and is about the
character-free TauCeti.cuspFormsOld N k.
The nebentypus of a level-raise at the exact level (cusp forms). The N = d * M case of
TauCeti.CuspForm.levelRaise_mem_cuspFormCharSpace_of_dvd.
The Γ₀(N/l)-transformation law of a function whose level-raise carries a nebentypus.
If the level-raise f ∣[k] V_l is an eigenvector of every γ ∈ Γ₀(N) with eigenvalue the value
χ reads off γ, if f is T-periodic, and if χ is trivial on the kernel of the reduction
(ZMod N)ˣ → (ZMod (N/l))ˣ, then f itself transforms under each γ' ∈ Γ₀(N / l) by χ u, for
any unit u of level N lying over the nebentypus label of γ'.
The value does not depend on which u is chosen: two such units differ by an element of the
kernel of the reduction, on which χ is trivial by hχ — which is exactly what that hypothesis
is for. TauCeti.slash_mapGL_eq_self_of_mem_Gamma1_div is the case of trivial label, and
TauCeti.cuspFormOfSmulSlashScaleGL_mem_cuspFormCharSpace is the case of a character that
factors, so both the descent and the nebentypus of the descended form are instances of this one
law rather than separate arguments.
Γ₁(N/l)-invariance from a nebentypus of level N that factors through N / l.
If the level-raise f ∣[k] V_l is an eigenvector of every γ ∈ Γ₀(N) with eigenvalue the
character value χ reads off γ, if f is T-periodic, and if χ is trivial on the kernel of
the reduction (ZMod N)ˣ → (ZMod (N/l))ˣ, then f is invariant under all of Γ₁(N / l).
This is the step that converts a nebentypus into honest invariance, and it is where the conductor
drops: a form whose character already factors through N / l is invariant under all of
Γ₁(N / l), the larger congruence subgroup at the lower level, which is what the conductor
argument turns into a statement about newforms.
Adapted from conductor_slash_eq_self_of_mem_Gamma1_div in AINTLIB
(Eigenforms/ConductorTheorem.lean:217, Chris Birkbeck, Apache-2.0, commit
2baa76f742bdb4fb8ee323fabba41203bd390e08). The source states it over its own levelRaiseFun
and a DirichletCharacter, and routes through a conductor-specific helper; here it is stated over
scaleGL and a units-valued character, and assembled from
exists_eq_T_zpow_mul_conjScale_mul_T_zpow,
slash_zpow_mul_mul_zpow_eq_smul and
slash_conjScale_eq_smul_of_slash_scaleGL.
The nebentypus character of a level restriction #
The nebentypus of a level restriction. For M ∣ N, reading a form of level M as a form
of level N carries M_k(Γ₁(M), χ) into M_k(Γ₁(N), χ ∘ (ZMod N)ˣ → (ZMod M)ˣ): the character
is pulled back along the reduction map.
This is the degeneracy map V₁ at the pair M ∣ N, the one operator the old subspace excludes
at M = N; unlike TauCeti.ModularForm.levelRaise_mem_modFormCharSpace, which raises the level
to exactly d * M, the target level here is an arbitrary multiple of M.
Follows restrictSubgroup_mem_modFormCharSpace of the AINTLIB LeanModularForms project
(Eigenforms/MainLemma.lean, https://github.com/CBirkbeck/AINTLIB, commit
2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0).
The nebentypus of a level restriction (cusp forms). For M ∣ N, reading a cusp form of
level M as a cusp form of level N carries S_k(Γ₁(M), χ) into
S_k(Γ₁(N), χ ∘ (ZMod N)ˣ → (ZMod M)ˣ). Together with TauCeti.ofLe_mem_cuspFormsOld this
places the restriction of a χ-form of proper divisor level inside the old subspace, with a
known character.
The q-expansion of a level-raise #
Scaling the argument by d raises the local parameter at the cusp ∞ to the d-th
power: q(d τ) = q(τ) ^ d.
The q-expansion of a level-raise. Level-raising substitutes q ↦ q ^ d in the
q-expansion, which on power series is PowerSeries.expand d.
The q-expansion of a level-raise, on coefficients. aₙ(V_d f) = a_{n/d}(f) when
d ∣ n, and 0 otherwise.
The q-expansion of a level-raise, at Γ₁. For f of level Γ₁(M), its image V_d f
has level Γ₁(dM) and q-expansion coefficients aₙ(V_d f) = a_{n/d}(f) when d ∣ n, and 0
otherwise.
The q-expansion of a level-raised cusp form. A cusp form and its image under the
inclusion into modular forms have the same underlying function, so the substitution q ↦ q ^ d
of ModularForm.qExpansion_levelRaise reads the same way on cusp forms.
The q-expansion of a level-raised cusp form, on coefficients.
aₙ(V_d f) = a_{n/d}(f) when d ∣ n, and 0 otherwise.
The q-expansion of a level-raised cusp form, at Γ₁. For f of level Γ₁(M), its
image V_d f has level Γ₁(dM) and q-expansion coefficients aₙ(V_d f) = a_{n/d}(f) when
d ∣ n, and 0 otherwise. These are the coefficients of the spanning forms of the old
subspace.
The coefficients of a level-raise, read backwards. If a cusp form G of level Γ₁(M)
is V_d g as a function on ℍ, that is ⇑G = d ^ (1 - k) • (⇑g ∣[k] diag(d, 1)) for a cusp
form g of level Γ₁(M / d) with d ∣ M, then a_m(g) = a_{dm}(G). This is how a form
recovered by the level-lowering dichotomy (ConductorDichotomy.lean) hands its coefficients
back.
Level-raising lands in the series supported on multiples of d. The q-expansion of
V_d f is the PowerSeries.expand d of that of f, so its coefficients away from the multiples
of d vanish.
This is the forward half of the Atkin–Lehner description of the old subspace: everything in the
image of V_d satisfies the support condition.
Level-raising lands in the series supported on multiples of d, for cusp forms. The
cusp-form reading of ModularForm.isSupportedOnDvd_qExpansion_levelRaise, which is the form the
old subspace is described with.