Character decomposition of modular forms for Γ₁(N)

For each character χ : (ZMod N)ˣ →* ℂˣ, the nebentypus character space modFormCharSpace k χ and its cusp-form analogue cuspFormCharSpace k χ are cut out in TauCeti/NumberTheory/ModularForms/DiamondOperators.lean as simultaneous diamond-eigenspaces. This file proves the internal direct sum decomposition

M_k(Γ₁(N)) = ⨁_{χ} M_k(Γ₁(N), χ)

together with its cusp-form analogues and the refinement to diamond-invariant submodules, by simultaneous diagonalization of the commuting finite-order diamond operators (TauCeti/LinearAlgebra/Eigenspace/JointEigenvector/Basic.lean).

The statements are unconditional, at every level N (including N = 0, where the diamond group is ℤˣ): the diamond group (ZMod N)ˣ is finite (instFiniteZModUnits, from Mathlib.Data.ZMod.Units) and commutative, so the classical character projectors decompose every vector (TauCeti.iSup_iInf_eigenspace_unitHom_eq_top_of_commGroup), with no finite-dimensionality hypotheses anywhere.

Ported from the AINTLIB LeanModularForms project (LeanModularForms/HeckeRIngs/GL2/CharacterDecomp.lean, Chris Birkbeck, https://github.com/CBirkbeck/AINTLIB/tree/main/projects/LeanModularForms), realizing Layer 0 of the ModularForms roadmap.

Main results

• iSup_modFormCharSpace_eq_top, iSup_cuspFormCharSpace_eq_top: the character spaces span M_k(Γ₁(N)) resp. S_k(Γ₁(N)).
• iSupIndep_modFormCharSpace, iSupIndep_cuspFormCharSpace: the families are supremum-independent.
• isInternal_modFormCharSpace, isInternal_cuspFormCharSpace: the DirectSum.IsInternal statements.
• iSup_inf_modFormCharSpace_of_invariant, iSup_inf_cuspFormCharSpace_of_invariant: any diamond-invariant submodule is the supremum of its intersections with the character spaces, with finsupp-indexed corollaries exists_finsupp_of_diamondOp_invariant/exists_finsupp_of_diamondOpCusp_invariant.
• linearMap_ext_of_mem_modFormCharSpace, linearMap_ext_of_mem_cuspFormCharSpace: two endomorphisms agreeing on every character space are equal — the gluing principle for extending Hecke-operator identities proven per character space to the whole space.

References

• Diamond–Shurman, A first course in modular forms, §5.2

theorem iSup_inf_modFormCharSpace_of_invariant {N : ℕ} (k : ℤ) (p : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)) (hp : ∀ (d : (ZMod N)ˣ), ∀ f ∈ p, ((diamondOpHom k) d) f ∈ p) : ⨆ (χ : (ZMod N)ˣ →* ℂˣ), p ⊓ modFormCharSpace k χ = p

Character decomposition of a diamond-invariant submodule of M_k(Γ₁(N)). If p ⊆ M_k(Γ₁(N)) is stable under every diamond operator ⟨d⟩ for d ∈ (ZMod N)ˣ, then p equals the supremum of its intersections with the nebentypus character subspaces modFormCharSpace k χ. Specializing p = ⊤ recovers iSup_modFormCharSpace_eq_top.

theorem iSup_inf_cuspFormCharSpace_of_invariant {N : ℕ} (k : ℤ) (p : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)) (hp : ∀ (d : (ZMod N)ˣ), ∀ f ∈ p, ((diamondOpCuspHom k) d) f ∈ p) : ⨆ (χ : (ZMod N)ˣ →* ℂˣ), p ⊓ cuspFormCharSpace k χ = p

Character decomposition of a diamond-invariant submodule of S_k(Γ₁(N)). The cusp-form analogue of iSup_inf_modFormCharSpace_of_invariant.

@[simp]

theorem iSup_modFormCharSpace_eq_top {N : ℕ} (k : ℤ) : ⨆ (χ : (ZMod N)ˣ →* ℂˣ), modFormCharSpace k χ = ⊤

The character subspaces modFormCharSpace k χ span the whole space: modular forms for Γ₁(N) decompose into the span of nebentypus character spaces, one for each character (ZMod N)ˣ →* ℂˣ.

theorem iSupIndep_modFormCharSpace {N : ℕ} (k : ℤ) : iSupIndep fun (χ : (ZMod N)ˣ →* ℂˣ) => modFormCharSpace k χ

The character subspaces form an independent family.

theorem isInternal_modFormCharSpace {N : ℕ} (k : ℤ) [DecidableEq ((ZMod N)ˣ →* ℂˣ)] : DirectSum.IsInternal fun (χ : (ZMod N)ˣ →* ℂˣ) => modFormCharSpace k χ

Internal direct sum decomposition: M_k(Γ₁(N)) decomposes as the direct sum of the nebentypus character spaces modFormCharSpace k χ.

theorem iSupIndep_cuspFormCharSpace {N : ℕ} (k : ℤ) : iSupIndep fun (χ : (ZMod N)ˣ →* ℂˣ) => cuspFormCharSpace k χ

The cusp-form character subspaces form an independent family.

@[simp]

theorem iSup_cuspFormCharSpace_eq_top {N : ℕ} (k : ℤ) : ⨆ (χ : (ZMod N)ˣ →* ℂˣ), cuspFormCharSpace k χ = ⊤

The cusp-form character subspaces span the whole space.

theorem isInternal_cuspFormCharSpace {N : ℕ} (k : ℤ) [DecidableEq ((ZMod N)ˣ →* ℂˣ)] : DirectSum.IsInternal fun (χ : (ZMod N)ˣ →* ℂˣ) => cuspFormCharSpace k χ

Internal direct sum decomposition of cusp forms: S_k(Γ₁(N)) decomposes as the direct sum of the nebentypus character spaces cuspFormCharSpace k χ.

theorem exists_finsupp_of_diamondOp_invariant {N : ℕ} (k : ℤ) (p : Submodule ℂ (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)) (hp : ∀ (d : (ZMod N)ˣ), ∀ f ∈ p, ((diamondOpHom k) d) f ∈ p) {f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ p) : ∃ (g : ((ZMod N)ˣ →* ℂˣ) →₀ ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k), (∀ (χ : (ZMod N)ˣ →* ℂˣ), g χ ∈ p ⊓ modFormCharSpace k χ) ∧ (g.sum fun (x : (ZMod N)ˣ →* ℂˣ) (y : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) => y) = f

Finsupp-indexed character decomposition of a modular form in a diamond-invariant submodule. Consumer-facing corollary of iSup_inf_modFormCharSpace_of_invariant: any element of a diamond-invariant submodule p ⊆ M_k(Γ₁(N)) is a finitely-supported sum of nebentypus-character components, each landing simultaneously in p and in its character subspace.

theorem exists_finsupp_of_diamondOpCusp_invariant {N : ℕ} (k : ℤ) (p : Submodule ℂ (CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k)) (hp : ∀ (d : (ZMod N)ˣ), ∀ f ∈ p, ((diamondOpCuspHom k) d) f ∈ p) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ p) : ∃ (g : ((ZMod N)ˣ →* ℂˣ) →₀ CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k), (∀ (χ : (ZMod N)ˣ →* ℂˣ), g χ ∈ p ⊓ cuspFormCharSpace k χ) ∧ (g.sum fun (x : (ZMod N)ˣ →* ℂˣ) (y : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k) => y) = f

Finsupp-indexed character decomposition of a cusp form in a diamond-invariant submodule. Cusp-form analogue of exists_finsupp_of_diamondOp_invariant.

theorem linearMap_ext_of_mem_modFormCharSpace {N : ℕ} {k : ℤ} {W : Type u_1} [AddCommMonoid W] [Module ℂ W] {S T : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k →ₗ[ℂ] W} (h : ∀ (χ : (ZMod N)ˣ →* ℂˣ), ∀ f ∈ modFormCharSpace k χ, S f = T f) : S = T

Extensionality along the character decomposition: two ℂ-linear maps out of M_k(Γ₁(N)) that agree on every nebentypus subspace modFormCharSpace k χ are equal. This is the gluing principle by which identities of Hecke operators proven per character space extend to the whole space of modular forms.

theorem linearMap_ext_of_mem_cuspFormCharSpace {N : ℕ} {k : ℤ} {W : Type u_1} [AddCommMonoid W] [Module ℂ W] {S T : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k →ₗ[ℂ] W} (h : ∀ (χ : (ZMod N)ˣ →* ℂˣ), ∀ f ∈ cuspFormCharSpace k χ, S f = T f) : S = T

Extensionality along the cusp-form character decomposition: two ℂ-linear maps out of S_k(Γ₁(N)) that agree on every nebentypus subspace cuspFormCharSpace k χ are equal.