Documentation

TauCeti.NumberTheory.ModularForms.ConductorDichotomy

The level-lowering dichotomy #

CuspDescent.lean builds the descent half of the conductor theorem: when the nebentypus χ is trivial on the kernel of (ZMod N)ˣ → (ZMod (N / l))ˣ, the function f whose level-raise is a cusp form of level N is itself a cusp form of level N / l. That is one horn of a dichotomy. This file supplies the other horn — when χ is not trivial on that kernel, f vanishes — and then puts the two together.

The shape of the vanishing argument #

The obstruction is read off a single unit. If χ is nontrivial on the kernel, pick u in the kernel with χ u ≠ 1, and lift it to Γ₀(N). Slashing f by the diag(l, 1)-conjugate of that lift multiplies f by χ u. But the same conjugate can be refactored: u may be replaced by any u' in its ZMod.unitsMap-coset at the cost of two translations T ^ i and T ^ j, and f is T-periodic, so the translations contribute nothing. Choosing u' with χ u' ≠ χ u — which is exactly what nontriviality on the kernel provides — exhibits f ∣[k] A as both χ u • f and χ u' • f for one matrix A. Two distinct multipliers for one slash force f = 0.

The refactoring step needs the lift's lower-left entry to be exactly N, not merely divisible by it, because conjScale l · c records the cofactor c and the argument compares the cofactors of two lifts. CongruenceSubgroup.gamma0Twist N p h is already such a lift, so a unit u is lifted by taking p to be the representative (u : ZMod N).val. Only the bottom row of that lift is specified, so the congruence between the upper-left entries of two of them — the shift T ^ i — is read off the determinants rather than off a formula for those entries.

Main results #

Implementation notes #

CuspDescent.lean carries its character as the units homomorphism (ZMod N)ˣ →* ℂˣ that cuspFormCharSpace is indexed by, with the descent hypothesis ∀ u, ZMod.unitsMap _ u = 1 → χ u = 1. The vanishing horn below is stated over the same homomorphism with the negation of that hypothesis, so the dichotomy is a by_cases on one proposition and neither horn has to restate the other's hypotheses. Only the final theorem is phrased over a DirichletCharacter, where FactorsThrough and the lowered character FactorsThrough.χ₀ live; the bridge between the two phrasings is mathlib's DirichletCharacter.factorsThrough_iff_ker_unitsMap.

References #

The lower-left entry of the Bézout twist #

Refactoring the conjugated lift through a separating unit #

The vanishing horn #

source
theorem TauCeti.eq_zero_of_not_forall_apply_eq_one_of_unitsMap_eq_one {N : ℕ} [NeZero N] {l : ℕ} [NeZero l] (hlN : l ∣ N) (k : ℤ) {χ : (ZMod N)ˣ →* ℂˣ} (hχ : ¬∀ (u : (ZMod N)ˣ), (ZMod.unitsMap ⋯) u = 1 → χ u = 1) (f : UpperHalfPlane → ℂ) (hnb : ∀ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (hγ : γ ∈ CongruenceSubgroup.Gamma0 N), SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) (SlashAction.map k (scaleGL l) f) = ↑(χ ((CongruenceSubgroup.Gamma0Map N).toHomUnits ⟨γ, hγ⟩)) • SlashAction.map k (scaleGL l) f) (hT : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ModularGroup.T) f = f) :
f = 0

The vanishing horn of the level-lowering dichotomy. If the nebentypus χ of the level-raise of f is not trivial on the kernel of (ZMod N)ˣ → (ZMod (N / l))ˣ, and f is T-periodic, then f = 0.

The hypotheses hnb and hT are exactly the ones TauCeti.slash_mapGL_eq_self_of_mem_Gamma1_div takes for the descent, and hχ is the negation of the triviality that TauCeti.cuspFormOfSmulSlashScaleGL assumes, so this is the complementary case of the descent and neither statement restates the other's hypotheses.

The dichotomy #

source
theorem TauCeti.cuspFormOfSmulSlashScaleGL_mem_cuspFormCharSpace {N : ℕ} [NeZero N] {l : ℕ} [NeZero l] (hlN : l ∣ N) (k : ℤ) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / l))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) (f : UpperHalfPlane → ℂ) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (hgχ : g ∈ cuspFormCharSpace k χ) (hg : ⇑g = ↑l ^ (1 - k) • SlashAction.map k (scaleGL l) f) (hT : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ModularGroup.T) f = f) :
cuspFormOfSmulSlashScaleGL l N hlN k χ ⋯ f g hgχ hg hT ∈ cuspFormCharSpace k χ₀

The descended cusp form carries the lowered nebentypus. cuspFormOfSmulSlashScaleGL produces a cusp form of level N / l; this identifies its nebentypus as any character χ₀ on ZMod (N / l) that χ pulls back from, which is the hypothesis hcomp, and that is what makes the descent an eigenform statement rather than merely a level statement. The dichotomy below specializes χ₀ to hfac.χ₀.

source
theorem TauCeti.exists_cuspForm_mem_cuspFormCharSpace_or_eq_zero {N : ℕ} [NeZero N] {l : ℕ} [NeZero l] (hlN : l ∣ N) (k : ℤ) (χ : DirichletCharacter ℂ N) (f : UpperHalfPlane → ℂ) (g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) (hgχ : g ∈ cuspFormCharSpace k (MulChar.toUnitHom χ)) (hg : ⇑g = ↑l ^ (1 - k) • SlashAction.map k (scaleGL l) f) (hT : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ModularGroup.T) f = f) :
(∃ (hfac : χ.FactorsThrough (N / l)), ∃ F ∈ cuspFormCharSpace k (MulChar.toUnitHom hfac.χ₀), ⇑F = f) ∨ f = 0

The level-lowering dichotomy. For l ∣ N, a Dirichlet character χ of level N, and a T-periodic f : ℍ → ℂ whose level-raise by l is a cusp form in S_k(N, χ): either χ factors through N / l and f is itself a cusp form in S_k(N / l, χ↓) for the lowered character, or f = 0.

This is Miyake's Theorem 4.6.4. The two horns are TauCeti.cuspFormOfSmulSlashScaleGL with TauCeti.cuspFormOfSmulSlashScaleGL_mem_cuspFormCharSpace, and TauCeti.eq_zero_of_not_forall_apply_eq_one_of_unitsMap_eq_one; the case split is on the single proposition that one assumes and the other negates.