The coefficient formula of the descent #
For a prime p ∣ N, a squarefree L coprime to p whose primes divide N, and a cusp form
f ∈ S_k(Γ₁(N), χ) whose nebentypus is pulled back from level N / p and which vanishes at
every index coprime to p L, the descent Φ = descendSlash k p N satisfies
a_m(Φ f) = (|family| / p) · a_m(g) for every m coprime to L,
where g is the coprime filter of f read at level L N / p. Rescaling by the nonzero
|family| = descendMatrixCount p N turns that into the descent witness: a cusp form
F ∈ S_k(Γ₁(N / p), χ₀) with a_m(F) = a_{pm}(f) at every m coprime to L — one prime
peeled off f, with its coefficients shifted by p. This is Miyake's Lemma 4.6.14, and the
inductive step of his Lemma 4.6.8.
The proof splits f = Δ + V_p g at level L N. The level-raise descends to
(|family| / p) • g (Descent/LevelRaise/Commute.lean), and the difference Δ vanishes at
every index coprime to L, so the squarefree decomposition writes it as ∑_{q ∈ l.primeFactors} V_q F_q (SquarefreeDecomposition.lean); the descent commutes with each V_q and kills it at
the indices coprime to L.
Main results #
TauCeti.qExpansion_coeff_descendSlash_eq_zero_of_coprime: the descent of a form vanishing at the indices coprime to a squarefreelagain vanishes there.TauCeti.qExpansion_coeff_descendSlash_eq_of_coprime: the coefficient formula above.TauCeti.exists_mem_cuspFormCharSpace_qExpansion_coeff_eq_coeff_mul_of_coprime: the descent witness.
Provenance #
Adapted from the AINTLIB LeanModularForms project (Chris Birkbeck, Apache-2.0,
https://github.com/CBirkbeck/AINTLIB @ eb9621e7bcb0ce220ad53983ec45d987cb5b9002),
projects/LeanModularForms/LeanModularForms/StrongMultiplicityOne/InductiveStep.lean —
miyake_4_6_14_coeff_formula with its delta_vanishing_* helpers, and the rescaling of
HeckeDescent.lean. The source keeps the descent as an explicit coset list and transports forms
across equalities of levels by casts; here the descent is descendSlash/descendCuspForm,
levels are related by divisibility, and the vanishing half is stated on its own so that the
squarefree decomposition enters once.
References #
- T. Miyake, Modular forms, Lemmas 4.6.8 and 4.6.14.
- F. Diamond and J. Shurman, A first course in modular forms, §5.7.
The descent of the difference vanishes at the indices coprime to L #
The descent of a form vanishing off l vanishes at the indices coprime to l (the core
of Miyake's Lemma 4.6.14). For Δ ∈ S_k(Γ₁(M), χ) with χ pulled back from χ₀ modulo M / p,
vanishing at every index coprime to a squarefree l coprime to p, the descent
descendSlash k p M Δ has a_m = 0 at every m coprime to l: Δ = ∑_{q ∣ l} V_q F_q, the
descent commutes with each V_q, and each V_q of a bundled descent is supported on the
multiples of q.
The coefficient formula of the descent #
The coefficients of the descent (Miyake, Lemma 4.6.14). Let f ∈ S_k(Γ₁(N), χ) with χ
pulled back from χ₀ modulo N / p, vanishing at every index coprime to p L for a squarefree
L coprime to p, and let g of level L N / p carry the coefficients of f along the
multiples of p: a_m(g) = a_{pm}(f) for m coprime to L, and a_m(g) = 0 otherwise. Then
at every m coprime to L, a_m(descendSlash k p N f) = (|family| / p) · a_m(g).
The descent witness #
The descent witness (Miyake, Lemma 4.6.8, the inductive step). For f ∈ S_k(Γ₁(N), χ)
with χ pulled back from χ₀ modulo N / p, vanishing at every index coprime to p L for a
squarefree L coprime to p whose primes divide N, there is F ∈ S_k(Γ₁(N / p), χ₀) with
a_m(F) = a_{pm}(f) at every m coprime to L: the descent of f, rescaled by
p / |family|, by the coefficient formula of the descent and the coprime-filter descent.