Documentation

TauCeti.NumberTheory.ModularForms.Newforms.Nebentypus

The old and new subspaces at a fixed nebentypus #

The old subspace S_k(Γ₁(N))ᵒˡᵈ and its Petersson-orthogonal complement, the new subspace S_k(Γ₁(N))ⁿᵉʷ (TauCeti/NumberTheory/ModularForms/Newforms/Basic.lean), are both stable under the diamond operators: the old one because the level-raising maps intertwine the diamonds, the new one because the diamonds are Petersson-unitary (TauCeti/NumberTheory/ModularForms/Petersson/Unitary.lean). Both therefore decompose along the nebentypus character spaces S_k(N, χ) = cuspFormCharSpace k χ, and this file records what that decomposition says about newness.

The main statement is the refinement at a fixed nebentypus: for a cusp form f ∈ S_k(N, χ), being new is orthogonality to the old forms of the same nebentypus alone,

f ∈ S_k(Γ₁(N))ⁿᵉʷ ↔ f ⊥ (S_k(Γ₁(N))ᵒˡᵈ ⊓ S_k(N, χ)),

because old forms of a different nebentypus are automatically orthogonal to f. Equivalently, in the form Layer 3 of the ModularForms roadmap asks for, the new subspace of S_k(N, χ) — the orthogonal complement, taken inside S_k(N, χ), of the old forms there — is S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ): newness may be read at level Γ₁(N) and then intersected. The old/new decomposition then restricts to each nebentypus space, S_k(N, χ) = S_k(N, χ)ᵒˡᵈ ⊕ S_k(N, χ)ⁿᵉʷ.

The old part of S_k(N, χ) is then described by its generators: it is spanned by the level-raises V_d S_k(M, ψ) from the proper divisor levels M, with d * M ∣ N, over the characters ψ modulo M whose pull-back to level N is χ. Such a ψ exists exactly when the conductor of χ divides M, and is then the descent χ_M of χ, so this is the description S_k(N, χ)ᵒˡᵈ = Σ_{M ∣ N, M ≠ N, cond χ ∣ M} Σ_{d ∣ N/M} V_d S_k(M, χ_M). The generators of S_k(Γ₁(N))ᵒˡᵈ with any other nebentypus land in the other character spaces, which are independent of S_k(N, χ). In particular, when χ is primitive no proper divisor level carries it, and every form in S_k(N, χ) is new.

Main results #

References #

Diamond stability of the new subspace #

source
theorem TauCeti.diamondOpCusp_mem_cuspFormsNew {N : ℕ} [NeZero N] {k : ℤ} (u : (ZMod N)ˣ) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsNew N k) :
(diamondOpCusp k u) f ∈ cuspFormsNew N k

The new subspace is diamond-stable. The old subspace is carried onto itself by ⟨u⟩, and ⟨u⟩ is Petersson-unitary, so it preserves the orthogonal complement as well.

source
theorem TauCeti.cuspFormsOldMultiples_map_diamondOpCusp_le {N : ℕ} [NeZero N] {k : ℤ} (u : (ZMod N)ˣ) (m : ℕ) :
Submodule.map (diamondOpCusp k u) (cuspFormsOldMultiples N k m) ≤ cuspFormsOldMultiples N k m

The refined old subspace is diamond-stable. ⟨u⟩ sends a level-raised newform to the level-raise of ⟨u'⟩ applied to it, where u' is the reduction of u; the new subspace at the smaller level is itself diamond-stable, and the level condition m ∣ M is untouched. So the generators are permuted among themselves.

source
theorem TauCeti.diamondOpCusp_mem_cuspFormsOldMultiples {N : ℕ} [NeZero N] {k : ℤ} (u : (ZMod N)ˣ) {m : ℕ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsOldMultiples N k m) :
(diamondOpCusp k u) f ∈ cuspFormsOldMultiples N k m

The refined old subspace is diamond-stable, in the membership form.

The nebentypus components of the old and new subspaces #

source
theorem TauCeti.iSup_inf_cuspFormsOld_cuspFormCharSpace (N : ℕ) [NeZero N] (k : ℤ) :
⨆ (χ : (ZMod N)ˣ →* ℂˣ), cuspFormsOld N k ⊓ cuspFormCharSpace k χ = cuspFormsOld N k

The old subspace is the sum of its nebentypus components.

source
theorem TauCeti.iSup_inf_cuspFormsNew_cuspFormCharSpace (N : ℕ) [NeZero N] (k : ℤ) :
⨆ (χ : (ZMod N)ˣ →* ℂˣ), cuspFormsNew N k ⊓ cuspFormCharSpace k χ = cuspFormsNew N k

The new subspace is the sum of its nebentypus components.

Newness at a fixed nebentypus #

source
theorem TauCeti.mem_cuspFormsNew_iff_of_mem_cuspFormCharSpace {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormCharSpace k χ) :
f ∈ cuspFormsNew N k ↔ f ∈ CuspForm.peterssonOrthogonal (cuspFormsOld N k ⊓ cuspFormCharSpace k χ)

Newness is tested against the old forms of the same nebentypus. A cusp form of nebentypus χ is new exactly when it is Petersson-orthogonal to the old forms of nebentypus χ: the old subspace is the sum of its nebentypus components, and the components with ψ ≠ χ are orthogonal to f for free, the nebentypus decomposition being an orthogonal one.

source
theorem TauCeti.cuspFormsNew_inf_cuspFormCharSpace (N : ℕ) [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) :
cuspFormsNew N k ⊓ cuspFormCharSpace k χ = CuspForm.peterssonOrthogonal (cuspFormsOld N k ⊓ cuspFormCharSpace k χ) ⊓ cuspFormCharSpace k χ

The new subspace of S_k(N, χ). The orthogonal complement of the old forms of nebentypus χ, taken inside S_k(N, χ), is what one gets by intersecting the new subspace of S_k(Γ₁(N)) with S_k(N, χ): newness may be read at level Γ₁(N) and then restricted to a nebentypus. This is the milestone S_k(N, χ)ⁿᵉʷ = S_k(Γ₁(N))ⁿᵉʷ ⊓ S_k(N, χ) of Layer 3 of the ModularForms roadmap.

source
theorem TauCeti.sup_cuspFormsOld_cuspFormsNew_inf_cuspFormCharSpace (N : ℕ) [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) :
cuspFormsOld N k ⊓ cuspFormCharSpace k χ ⊔ cuspFormsNew N k ⊓ cuspFormCharSpace k χ = cuspFormCharSpace k χ

The old/new decomposition restricts to each nebentypus space: S_k(N, χ) is spanned by its old and its new part. Inside S_k(N, χ) the two are complementary, by the modular law and the completeness of the Petersson-orthogonal complement.

source
theorem TauCeti.disjoint_cuspFormsOld_cuspFormsNew_inf_cuspFormCharSpace (N : ℕ) [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) :
Disjoint (cuspFormsOld N k ⊓ cuspFormCharSpace k χ) (cuspFormsNew N k ⊓ cuspFormCharSpace k χ)

The old and new parts of S_k(N, χ) meet only in 0.

The old part of S_k(N, χ) by nebentypus #

source
theorem TauCeti.levelRaise_mem_cuspFormsOld_inf_cuspFormCharSpace {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {M d : ℕ} [NeZero d] (h : d * M ∣ N) (hM : M ≠ N) {ψ : (ZMod M)ˣ →* ℂˣ} (hχ : χ = ψ.comp (ZMod.unitsMap ⋯)) {g : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 M)) k} (hg : g ∈ cuspFormCharSpace k ψ) :
CuspForm.levelRaise d ⋯ g ∈ cuspFormsOld N k ⊓ cuspFormCharSpace k χ

Introduction rule for the old part of S_k(N, χ). The level-raise V_d g of a form g ∈ S_k(M, ψ) of proper divisor level M, with d * M ∣ N and χ the pull-back of ψ along (ZMod N)ˣ → (ZMod M)ˣ, is an old form of nebentypus χ.

source
theorem TauCeti.cuspFormsOld_inf_cuspFormCharSpace_le {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {V : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)} (hV : ∀ (M d : ℕ) [inst : NeZero d] (h : d * M ∣ N), M ≠ N → ∀ (ψ : (ZMod M)ˣ →* ℂˣ), χ = ψ.comp (ZMod.unitsMap ⋯) → ∀ g ∈ cuspFormCharSpace k ψ, CuspForm.levelRaise d ⋯ g ∈ V) :
cuspFormsOld N k ⊓ cuspFormCharSpace k χ ≤ V

Elimination rule for the old part of S_k(N, χ). A subspace containing every level-raise V_d g of a form g ∈ S_k(M, ψ) of proper divisor level M, for every character ψ modulo M whose pull-back to level N is χ, contains every old form of nebentypus χ.

Only the generators of the old subspace with the right nebentypus are tested: the old subspace is spanned by the V_d images of the character spaces S_k(M, ψ), the image of S_k(M, ψ) lies in S_k(N, ψ ∘ unitsMap), and the character spaces of S_k(Γ₁(N)) are independent, so the generators of any other nebentypus contribute nothing to S_k(N, χ).

source
theorem TauCeti.cuspFormsOld_inf_cuspFormCharSpace_eq_iSup (N : ℕ) [NeZero N] (k : ℤ) (χ : (ZMod N)ˣ →* ℂˣ) :
cuspFormsOld N k ⊓ cuspFormCharSpace k χ = ⨆ (M : ℕ), ⨆ (d : ℕ), ⨆ (h : d * M ∣ N ∧ M ≠ N), ⨆ (ψ : (ZMod M)ˣ →* ℂˣ), ⨆ (_ : χ = ψ.comp (ZMod.unitsMap ⋯)), Submodule.map (CuspForm.levelRaiseₗ d ⋯) (cuspFormCharSpace k ψ)

The old part of S_k(N, χ) by nebentypus. The old forms of nebentypus χ are exactly the span of the level-raises V_d S_k(M, ψ) over the proper divisor levels M with d * M ∣ N and the characters ψ modulo M pulling back to χ. Such a ψ is unique when it exists, since (ZMod N)ˣ → (ZMod M)ˣ is onto, and it exists exactly when the Dirichlet character of χ factors through M, that is, when its conductor divides M (DirichletCharacter.exists_eq_comp_unitsMap_of_factorsThrough, DirichletCharacter.changeLevel_factorsThrough and DirichletCharacter.mem_conductorSet_iff_conductor_dvd). So this is the description S_k(N, χ)ᵒˡᵈ = Σ_{M ∣ N, M ≠ N, cond χ ∣ M} Σ_{d ∣ N / M} V_d S_k(M, χ_M) of the old forms of nebentypus χ by generators, as in Miyake, §4.6.

source
theorem TauCeti.cuspFormsOld_inf_cuspFormCharSpace_eq_bot_of_isPrimitive {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (hχ : DirichletCharacter.IsPrimitive (MulChar.ofUnitHom χ)) :
cuspFormsOld N k ⊓ cuspFormCharSpace k χ = ⊥

A primitive nebentypus has no old forms. If the Dirichlet character of χ is primitive of conductor N, it is pulled back from no proper divisor level, so S_k(N, χ) contains no old form.

source
theorem TauCeti.cuspFormCharSpace_le_cuspFormsNew_of_isPrimitive {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} (hχ : DirichletCharacter.IsPrimitive (MulChar.ofUnitHom χ)) :
cuspFormCharSpace k χ ≤ cuspFormsNew N k

Every form of primitive nebentypus is new. If the Dirichlet character of χ is primitive of conductor N, then S_k(N, χ) ≤ S_k(Γ₁(N))ⁿᵉʷ: the old part of S_k(N, χ) vanishes (cuspFormsOld_inf_cuspFormCharSpace_eq_bot_of_isPrimitive), and S_k(N, χ) is the sum of its old and new parts.