The descent slash sum is Γ₀(N / p)-invariant

Newforms/Descent/Action.lean shows that, at a prime p ∣ N, right multiplication by γ ∈ Γ₀(N / p) permutes the family descendMatrix p N up to Γ₀(N) — by descendShift when p² ∣ N, by descendIndexShift when p exactly divides N. This file draws the consequence that the descent consumes: if f transforms under Γ₀(N) by a scalar, the sum of the slashes of f along the family transforms under Γ₀(N / p) by that scalar; in particular the sum is Γ₀(N / p)-invariant whenever f is Γ₀(N)-invariant.

Main definitions

• TauCeti.descendSlash: ∑ v, f ∣[k] descendMatrix p N v, the descent slash sum.

Main results

• TauCeti.descendSlash_zero, TauCeti.descendSlash_add, TauCeti.descendSlash_smul, TauCeti.descendSlash_finsetSum: f ↦ descendSlash k p N f is linear.
• TauCeti.descendSlash_eq_heckeSlashUpperTri: for p² ∣ N the descent slash sum is the upper-triangular Hecke sum heckeSlashUpperTri k p, the operator U_p on functions.
• TauCeti.descendSlash_slash_mapGL_of_mem_Gamma0: for p² ∣ N and γ ∈ Γ₀(N / p), if f ∣[k] δ = u • f for every δ ∈ Γ₀(N) with the lower-right entry of γ modulo N / p, then descendSlash k p N f ∣[k] γ = u • descendSlash k p N f, for a scalar u from any α acting compatibly on ℂ.
• TauCeti.descendSlash_slash_mapGL_eq_self_of_mem_Gamma0: its case u = 1 — the descent sum of a Γ₀(N)-invariant function is Γ₀(N / p)-invariant.
• TauCeti.descendSlash_slash_mapGL_of_nebentypus: if f transforms under Γ₀(N) by χ, and χ is the pull-back of χ₀ modulo N / p, then descendSlash k p N f transforms under Γ₀(N / p) by χ₀ — the descent lowers the level of the nebentypus.
• TauCeti.descendSlash_slash_mapGL_of_mem_Gamma0_of_prime, TauCeti.descendSlash_slash_mapGL_eq_self_of_mem_Gamma0_of_prime, TauCeti.descendSlash_slash_mapGL_of_nebentypus_of_prime: the three statements at every prime p ∣ N, the p² ∣ N case above and the p ∥ N case (a private lemma, with the family permuted by descendIndexShift) combined.

Scope

The behaviour at cusps is not claimed; it is Newforms/Descent/Cusps.lean.

Corresponds to miyake_hecke_descend_char in the AINTLIB LeanModularForms project (LeanModularForms/StrongMultiplicityOne/HeckeDescent.lean, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms).

noncomputable def TauCeti.descendSlash (k : ℤ) (p N : ℕ) [NeZero p] (f : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

The descent slash sum: ∑ v, f ∣[k] descendMatrix p N v, over the whole family.

Equations

• TauCeti.descendSlash k p N f = ∑ v : Fin (TauCeti.descendMatrixCount p N), SlashAction.map k (TauCeti.descendMatrix p N v) f

theorem TauCeti.descendSlash_def (k : ℤ) (p N : ℕ) [NeZero p] (f : UpperHalfPlane → ℂ) : descendSlash k p N f = ∑ v : Fin (descendMatrixCount p N), SlashAction.map k (descendMatrix p N v) f

The defining equation of descendSlash: the sum of the slashes of f along the family.

theorem TauCeti.descendSlash_apply (k : ℤ) (p N : ℕ) [NeZero p] (f : UpperHalfPlane → ℂ) (τ : UpperHalfPlane) : descendSlash k p N f τ = ∑ v : Fin (descendMatrixCount p N), SlashAction.map k (descendMatrix p N v) f τ

The value of the descent slash sum at a point: the sum of the slashed values.

theorem TauCeti.mdifferentiable_descendSlash (k : ℤ) (p N : ℕ) [NeZero p] {f : UpperHalfPlane → ℂ} (hf : MDiff f) : MDiff (descendSlash k p N f)

The descent slash sum of a holomorphic function is holomorphic: each slash is.

@[simp]

theorem TauCeti.descendSlash_zero (k : ℤ) (p N : ℕ) [NeZero p] : descendSlash k p N 0 = 0

The descent slash sum sends the zero function to zero.

@[simp]

theorem TauCeti.descendSlash_add (k : ℤ) (p N : ℕ) [NeZero p] (f g : UpperHalfPlane → ℂ) : descendSlash k p N (f + g) = descendSlash k p N f + descendSlash k p N g

The descent slash sum is additive in f, since each slash is.

@[simp]

theorem TauCeti.descendSlash_smul (k : ℤ) (p N : ℕ) [NeZero p] {α : Type u_1} [DistribSMul α ℂ] [IsScalarTower α ℂ ℂ] (c : α) (f : UpperHalfPlane → ℂ) : descendSlash k p N (c • f) = c • descendSlash k p N f

Scalars pass through the descent slash sum. With descendSlash_add and descendSlash_zero this is the linearity of f ↦ descendSlash k p N f; the scalar generality matches ModularForm.smul_slash_of_det_pos, which applies because every member of the family has positive determinant (descendMatrix_det_pos).

@[simp]

theorem TauCeti.descendSlash_finsetSum (k : ℤ) (p N : ℕ) [NeZero p] {ι : Type u_1} (s : Finset ι) (f : ι → UpperHalfPlane → ℂ) : descendSlash k p N (∑ i ∈ s, f i) = ∑ i ∈ s, descendSlash k p N (f i)

The descent slash sum commutes with a finite sum, the Finset.sum form of descendSlash_add and descendSlash_zero.

theorem TauCeti.descendSlash_eq_heckeSlashUpperTri {p N : ℕ} (k : ℤ) [NeZero p] (hpsq : p ^ 2 ∣ N) (f : UpperHalfPlane → ℂ) : descendSlash k p N f = HeckeRing.GL2.heckeSlashUpperTri k p f

At p² ∣ N the descent slash sum is the upper-triangular Hecke sum ∑ b < p, f ∣[k] [1, b; 0, p]: the family then has exactly its p upper-triangular members. So at p² ∣ N the descent is the bad-prime operator U_p on underlying functions.

theorem TauCeti.descendSlash_slash_mapGL_of_mem_Gamma0 {p N : ℕ} (k : ℤ) [NeZero p] (hpsq : p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 (N / p)) {α : Type u_1} [DistribSMul α ℂ] [IsScalarTower α ℂ ℂ] {f : UpperHalfPlane → ℂ} {u : α} (hf : ∀ δ ∈ CongruenceSubgroup.Gamma0 N, ↑(↑δ 1 1) = ↑(↑γ 1 1) → SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) δ) f = u • f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) (descendSlash k p N f) = u • descendSlash k p N f

The descent slash sum is Γ₀(N / p)-equivariant at p² ∣ N. If f ∣[k] δ = u • f for every δ ∈ Γ₀(N) with the same lower-right entry modulo N / p as γ ∈ Γ₀(N / p), then descendSlash k p N f ∣[k] γ = u • descendSlash k p N f. With u = 1 this is the Γ₀(N / p)-invariance of the descent sum of a Γ₀(N)-invariant function; with u a character value it is the nebentypus transport descendSlash_slash_mapGL_of_nebentypus. The scalar may come from any α acting compatibly on ℂ, as in descendSlash_smul.

theorem TauCeti.descendSlash_slash_mapGL_eq_self_of_mem_Gamma0 {p N : ℕ} (k : ℤ) [NeZero p] (hpsq : p ^ 2 ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 (N / p)) {f : UpperHalfPlane → ℂ} (hf : ∀ δ ∈ CongruenceSubgroup.Gamma0 N, SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) δ) f = f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) (descendSlash k p N f) = descendSlash k p N f

The descent slash sum is Γ₀(N / p)-invariant at p² ∣ N: if f is invariant under Γ₀(N), then descendSlash k p N f is invariant under the larger group Γ₀(N / p) — the descent lowers the level. The case u = 1 of descendSlash_slash_mapGL_of_mem_Gamma0.

theorem TauCeti.descendSlash_slash_mapGL_of_nebentypus {p N : ℕ} (k : ℤ) [NeZero p] (hpsq : p ^ 2 ∣ N) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) (γ : ↥(CongruenceSubgroup.Gamma0 (N / p))) {f : UpperHalfPlane → ℂ} (hf : ∀ (δ : ↥(CongruenceSubgroup.Gamma0 N)), SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ↑δ) f = ↑(χ ((CongruenceSubgroup.Gamma0Map N).toHomUnits δ)) • f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ↑γ) (descendSlash k p N f) = ↑(χ₀ ((CongruenceSubgroup.Gamma0Map (N / p)).toHomUnits γ)) • descendSlash k p N f

The descent sum lowers the level of the nebentypus at p² ∣ N. If f transforms under Γ₀(N) by χ, and χ is the pull-back of a character χ₀ modulo N / p (the hypothesis hcomp, in the shape cuspFormOfSmulSlashScaleGL_mem_cuspFormCharSpace takes), then descendSlash k p N f transforms under Γ₀(N / p) by χ₀.

theorem TauCeti.descendSlash_slash_mapGL_of_mem_Gamma0_of_prime {p N : ℕ} (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 (N / p)) {α : Type u_1} [DistribSMul α ℂ] [IsScalarTower α ℂ ℂ] {f : UpperHalfPlane → ℂ} {u : α} (hf : ∀ δ ∈ CongruenceSubgroup.Gamma0 N, ↑(↑δ 1 1) = ↑(↑γ 1 1) → SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) δ) f = u • f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) (descendSlash k p N f) = u • descendSlash k p N f

The descent slash sum is Γ₀(N / p)-equivariant at every prime p ∣ N: the case p² ∣ N is descendSlash_slash_mapGL_of_mem_Gamma0; when p exactly divides N the family is permuted by descendIndexShift instead.

theorem TauCeti.descendSlash_slash_mapGL_eq_self_of_mem_Gamma0_of_prime {p N : ℕ} (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ} (hγ : γ ∈ CongruenceSubgroup.Gamma0 (N / p)) {f : UpperHalfPlane → ℂ} (hf : ∀ δ ∈ CongruenceSubgroup.Gamma0 N, SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) δ) f = f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) γ) (descendSlash k p N f) = descendSlash k p N f

The descent slash sum is Γ₀(N / p)-invariant at every prime p ∣ N: the case u = 1 of descendSlash_slash_mapGL_of_mem_Gamma0_of_prime.

theorem TauCeti.descendSlash_slash_mapGL_of_nebentypus_of_prime {p N : ℕ} (k : ℤ) (hp : Nat.Prime p) (hpN : p ∣ N) {χ : (ZMod N)ˣ →* ℂˣ} {χ₀ : (ZMod (N / p))ˣ →* ℂˣ} (hcomp : χ = χ₀.comp (ZMod.unitsMap ⋯)) (γ : ↥(CongruenceSubgroup.Gamma0 (N / p))) {f : UpperHalfPlane → ℂ} (hf : ∀ (δ : ↥(CongruenceSubgroup.Gamma0 N)), SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ↑δ) f = ↑(χ ((CongruenceSubgroup.Gamma0Map N).toHomUnits δ)) • f) : SlashAction.map k ((Matrix.SpecialLinearGroup.mapGL ℝ) ↑γ) (descendSlash k p N f) = ↑(χ₀ ((CongruenceSubgroup.Gamma0Map (N / p)).toHomUnits γ)) • descendSlash k p N f

The descent sum lowers the level of the nebentypus at every prime p ∣ N: the every-prime form of descendSlash_slash_mapGL_of_nebentypus.