A form with a periodic level-l descent is old

Let l be a divisor of N other than 1, and let φ : ℍ → ℂ be invariant under the weight-k slash action of T. If the level-raise l ^ (1 - k) • (φ ∣[k] diag(l, 1)) is a cusp form f of level Γ₁(N) lying in the nebentypus space S_k(N, χ), then f is old.

ConductorDichotomy.lean proves Miyake's Theorem 4.6.4 under exactly those hypotheses: either χ factors through N / l and φ is itself a cusp form of level Γ₁(N / l), or φ is identically zero. Both horns say the same thing about f. On the first it is the level-raise V_l F of a genuine cusp form of the proper divisor level N / l; on the second it is 0; and TauCeti.cuspFormsOld contains both.

Why l ≠ 1 is the only arithmetic hypothesis

TauCeti.cuspFormsOld is spanned by the level-raises from proper divisor levels, so what the argument needs of l is exactly that N / l be a proper divisor of N — that is, l ≠ 1, which together with l ∣ N and N ≠ 0 gives N / l < N. Neither result asks l to be prime.

The two entry points differ in where the descent comes from. mem_cuspFormsOld_of_slash_T_eq takes φ from the caller, so no hypothesis on the q-expansion of f appears in it at all; mem_cuspFormsOld_of_qExpansionSupportedOnDvd instead assumes QExpansionSupportedOnDvd l f and obtains φ from it.

Main results

• TauCeti.mem_cuspFormsOld_of_slash_T_eq: a cusp form of level Γ₁(N) with a nebentypus, whose level-l descent is invariant under the weight-k slash action of T, is old.
• TauCeti.exists_eq_levelRaise_of_mem_qSupportedOnDvdSubmodule: a supported form in one nebentypus space is an actual V_l-image from level N / l.
• TauCeti.mem_cuspFormsOld_of_qExpansionSupportedOnDvd: the Atkin–Lehner step at one divisor — the same conclusion from the q-expansion support condition alone, the descent being supplied by Newforms/Descent/Basic.lean.
• TauCeti.qSupportedOnDvdSubmodule_inf_cuspFormCharSpace_eq_range_inf: the exact subspace characterization of supported forms at a fixed nebentypus.

Provenance

Adapted from AINTLIB (Chris Birkbeck, Apache-2.0) at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, projects/LeanModularForms/LeanModularForms/Eigenforms/AtkinLehner.lean — the case split of qSupportedOnDvd_mem_cuspFormsOld_of_char (lines 169-192).

References

• F. Diamond and J. Shurman, A first course in modular forms, Section 5.6.
• Miyake, Modular forms, Section 4.6 (Theorem 4.6.4 is the dichotomy consumed here).

theorem TauCeti.mem_cuspFormsOld_of_slash_T_eq {N : ℕ} [NeZero N] {k : ℤ} {l : ℕ} (hl : l ≠ 1) (hlN : l ∣ N) (χ : DirichletCharacter ℂ N) (φ : UpperHalfPlane → ℂ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hfχ : f ∈ cuspFormCharSpace k (MulChar.toUnitHom χ)) (hf : ⇑f = ↑l ^ (1 - k) • SlashAction.map k (scaleGL l) φ) (hT : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ModularGroup.T) φ = φ) : f ∈ cuspFormsOld N k

A cusp form with a T-periodic level-l descent is old. If f ∈ S_k(N, χ) is the level-raise l ^ (1 - k) • (φ ∣[k] diag(l, 1)) of a function φ : ℍ → ℂ invariant under the weight-k slash action of T, and l is a divisor of N other than 1, then f lies in the old subspace S_k(Γ₁(N))ᵒˡᵈ.

This is the level-lowering dichotomy TauCeti.exists_cuspForm_mem_cuspFormCharSpace_or_eq_zero read for its common conclusion: on the descent horn φ is a cusp form of level Γ₁(N / l) and f is its level-raise, and on the vanishing horn φ = 0 forces f = 0. Both are old.

theorem TauCeti.exists_eq_levelRaise_of_mem_qSupportedOnDvdSubmodule {N : ℕ} [NeZero N] {k : ℤ} {l : ℕ} [NeZero l] (hlN : l ∣ N) (χ : (ZMod N)ˣ →* ℂˣ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hfχ : f ∈ cuspFormCharSpace k χ) (hf : f ∈ qSupportedOnDvdSubmodule N k l) : ∃ (F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 (N / l))) k), f = CuspForm.levelRaise l ⋯ F

A supported form is a degeneracy image from the quotient level. If a cusp form in a nebentypus space has its period-one q-expansion supported on multiples of l, for l ∣ N, then it is V_l F for a cusp form F of level N / l. The character either descends to that level, in which case the level-lowering dichotomy supplies F, or forces the descended function to vanish, in which case F = 0 works.

theorem TauCeti.mem_cuspFormsOld_of_qExpansionSupportedOnDvd {N : ℕ} [NeZero N] {k : ℤ} {l : ℕ} (hl : l ≠ 1) (hlN : l ∣ N) (χ : DirichletCharacter ℂ N) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hfχ : f ∈ cuspFormCharSpace k (MulChar.toUnitHom χ)) (hf : QExpansionSupportedOnDvd l f) : f ∈ cuspFormsOld N k

The Atkin–Lehner step at one divisor. A cusp form of level Γ₁(N) with a nebentypus, whose period-one q-expansion is supported on the multiples of a divisor l ≠ 1 of N, is old.

The support condition is the only thing asked of the q-expansion, and l need not be prime.

⚠ The hypothesis is support on the multiples of one divisor l, for a form in one character space. Diamond–Shurman Theorem 5.7.1 assumes instead that aₙ(f) = 0 at every n coprime to N, a condition naming no divisor. The two are not interchangeable, and the implication runs one way: since l ∣ N and l ≠ 1, every n coprime to N is in particular not divisible by l, so QExpansionSupportedOnDvd l is the stronger hypothesis — it kills every index off the multiples of l, not merely those prime to N. The two agree only in the degenerate case where l is prime and N is a power of l: if they agree then every prime q dividing N satisfies l ∣ q, forcing q = l. Getting from Diamond–Shurman's hypothesis to this one therefore means splitting f across the primes dividing N.

theorem TauCeti.qSupportedOnDvdSubmodule_inf_cuspFormCharSpace_eq_range_inf {N : ℕ} [NeZero N] {k : ℤ} {l : ℕ} [NeZero l] (hlN : l ∣ N) (χ : (ZMod N)ˣ →* ℂˣ) : qSupportedOnDvdSubmodule N k l ⊓ cuspFormCharSpace k χ = (CuspForm.levelRaiseₗ l ⋯).range ⊓ cuspFormCharSpace k χ

Supported forms of fixed nebentypus are exactly the degeneracy images with that nebentypus. Intersecting the forms supported on multiples of l with S_k(N, χ) gives the intersection of S_k(N, χ) with the range of V_l from level N / l. No character is chosen on the source: the target intersection records exactly the transformation law needed at level N.