The Hecke eigenbasis and Eisenstein eigenform at level one

At level one, the congruence subgroup (Gamma1 1).map (mapGL ℝ) equals the full modular group 𝒮ℒ (Gamma1_one_map_eq_SL), there are no oldforms (cuspFormsNew_one), and (ZMod 1)ˣ is trivial, so every form has trivial nebentypus. Transporting the Atkin–Lehner–Miyake–Li newform basis HeckeRing.GL2.Newform.basis 1 k along this group equality equips CuspForm 𝒮ℒ k with a canonical basis levelOneNewformBasis k indexed by Newform 1 k.

Because the level-one Hecke operators heckeTLevelOne and heckeTCuspLevelOne share the positive Fourier-coefficient divisor-sum formula with the composite Hecke-ring elements heckeTCompositeGamma0 1 n acting at trivial character, the two actions agree across modularFormGamma1OneEquiv (for k ≠ 0) and cuspFormGamma1OneEquiv (at every weight). From this comparison we obtain:

• commutativity of the level-one Hecke operators heckeTCuspLevelOne and heckeTLevelOne;
• simultaneous diagonalization of heckeTCuspLevelOne k n on levelOneNewformBasis k, with eigenvalue the n-th Fourier coefficient (qExpansion 1 f.toCuspForm).coeff n, and the trace formula Tr(Tₙ | S_k) = ∑_{f ∈ Newform 1 k} aₙ(f);
• the identities T₁ = 1 and T_{p^{r+2}} = Tₚ T_{p^{r+1}} - p^{k-1} T_{p^r} between the operators heckeTCuspLevelOne, read off on this basis from the normalization a₁ = 1 and the prime-power recurrence of the coefficients of a newform;
• separation of coordinates in any subspace of CuspForm 𝒮ℒ k stable under Tₚ for every prime p (levelOneNewformBasis_mem_of_forall_prime), combining multiplicity one at level one with Module.Basis.self_mem_of_repr_ne_zero_of_forall, and the resulting prime-Hecke injectivity criterion injective_of_heckeTCuspLevelOne_mem_ker;
• the Hecke eigenform equation Tₙ(E_k) = σ_{k-1}(n) E_k for the normalized Eisenstein series ModularForm.E hk at even weight k ≥ 4 (heckeTLevelOne_E), deduced from the multiplicativity and prime-power recurrence of σ_{k-1} via forall_heckeTCompositeGamma0_eq_coeff_smul_iff, together with the direct-sum decomposition M_k(SL(2, ℤ)) = S_k(SL(2, ℤ)) ⊕ ℂ · E_k and the resulting trace identity Tr(Tₙ | M_k) = Tr(Tₙ | S_k) + σ_{k-1}(n).

Main definitions

• TauCeti.modularFormGamma1OneEquiv, TauCeti.cuspFormGamma1OneEquiv: the ℂ-linear equivalences M_k(Γ₁(1)) ≃ₗ[ℂ] M_k(SL(2, ℤ)) and S_k(Γ₁(1)) ≃ₗ[ℂ] S_k(SL(2, ℤ)) preserving underlying functions on ℍ.
• TauCeti.levelOneNewformBasis: the basis of CuspForm 𝒮ℒ k indexed by Newform 1 k.

Main results

• TauCeti.heckeTCuspLevelOne_cuspFormGamma1OneEquiv, TauCeti.heckeTLevelOne_modularFormGamma1OneEquiv: compatibility of heckeTCuspLevelOne and heckeTLevelOne with heckeTCompositeGamma0 1 n.
• TauCeti.commute_heckeTCuspLevelOne, TauCeti.commute_heckeTLevelOne: level-one Hecke operators commute.
• HeckeRing.GL2.Newform.twelve_le_weight, TauCeti.heckeTCuspLevelOne_levelOneNewformBasis, TauCeti.trace_heckeTCuspLevelOne, TauCeti.levelOneNewformBasis_mem_of_forall_prime, TauCeti.injective_of_heckeTCuspLevelOne_mem_ker: the weight bound 12 ≤ k on level-one newforms, eigenbasis action, trace, prime-Hecke invariant-subspace coordinate extraction, and injectivity criterion on CuspForm 𝒮ℒ k.
• TauCeti.heckeTCuspLevelOne_one, TauCeti.heckeTCuspLevelOne_prime_pow_add_two: T₁ = 1 and the recurrence T_{p^{r+2}} = Tₚ T_{p^{r+1}} - p^{k-1} T_{p^r} on CuspForm 𝒮ℒ k.
• TauCeti.heckeTLevelOne_E, TauCeti.isCompl_cuspFormSubmodule_span_E, TauCeti.trace_heckeTLevelOne: the Eisenstein Hecke eigenvalue, the cusp/Eisenstein complement, and the trace of Tₙ on ModularForm 𝒮ℒ k.

References

• J.-P. Serre, A course in arithmetic, Chapter VII, §§4–5.
• F. Diamond and J. Shurman, A first course in modular forms, Propositions 5.2.3, 5.3.1, and 5.8.5, and Theorem 5.8.2.

Re-reading Γ₁(1) forms as SL(2, ℤ) forms

def TauCeti.modularFormGamma1OneEquiv (k : ℤ) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k ≃ₗ[ℂ] ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

Modular forms for Γ₁(1) and for SL(2, ℤ) are canonically linearly isomorphic, via the subgroup equality Gamma1_one_map_eq_SL, without changing the underlying function on ℍ.

@[simp]

theorem ModularForm.coe_modularFormGamma1OneEquiv_apply {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k) : ⇑((TauCeti.modularFormGamma1OneEquiv k) f) = ⇑f

modularFormGamma1OneEquiv preserves the underlying function on ℍ.

@[simp]

theorem ModularForm.coe_modularFormGamma1OneEquiv_symm_apply {k : ℤ} (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ⇑((TauCeti.modularFormGamma1OneEquiv k).symm f) = ⇑f

The inverse of modularFormGamma1OneEquiv preserves the underlying function on ℍ.

def TauCeti.cuspFormGamma1OneEquiv (k : ℤ) : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k ≃ₗ[ℂ] CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k

Cusp forms for Γ₁(1) and for SL(2, ℤ) are canonically linearly isomorphic, via the subgroup equality Gamma1_one_map_eq_SL, without changing the underlying function on ℍ.

@[simp]

theorem CuspForm.coe_cuspFormGamma1OneEquiv_apply {k : ℤ} (f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k) : ⇑((TauCeti.cuspFormGamma1OneEquiv k) f) = ⇑f

cuspFormGamma1OneEquiv preserves the underlying function on ℍ.

@[simp]

theorem CuspForm.coe_cuspFormGamma1OneEquiv_symm_apply {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ⇑((TauCeti.cuspFormGamma1OneEquiv k).symm f) = ⇑f

The inverse of cuspFormGamma1OneEquiv preserves the underlying function on ℍ.

theorem ModularForm.mem_modFormCharSpace_one_level_one {k : ℤ} (F : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k) : F ∈ TauCeti.modFormCharSpace k 1

Every Γ₁(1) modular form lies in the trivial-character subspace M_k(Γ₁(1), 1).

theorem CuspForm.mem_cuspFormCharSpace_one_level_one {k : ℤ} (F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k) : F ∈ TauCeti.cuspFormCharSpace k 1

Every Γ₁(1) cusp form lies in the trivial-character subspace S_k(Γ₁(1), 1).

@[simp]

theorem TauCeti.modFormCharSpace_one_level_one (k : ℤ) : modFormCharSpace k 1 = ⊤

At level one every modular form has trivial nebentypus.

@[simp]

theorem TauCeti.cuspFormCharSpace_one_level_one (k : ℤ) : cuspFormCharSpace k 1 = ⊤

At level one every cusp form has trivial nebentypus.

Compatibility of heckeTLevelOne and heckeTCuspLevelOne with heckeTCompositeGamma0 1

theorem TauCeti.heckeTCuspLevelOne_cuspFormGamma1OneEquiv (k : ℤ) (n : ℕ) [NeZero n] (F : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k) : (heckeTCuspLevelOne k n) ((cuspFormGamma1OneEquiv k) F) = (cuspFormGamma1OneEquiv k) ↑(((HeckeRing.GL2.heckeRingHomCuspCharSpace k 1) (HeckeRing.GL2.heckeTCompositeGamma0 1 n)) ⟨F, ⋯⟩)

Compatibility of heckeTCuspLevelOne with the composite Γ₀(1) Hecke action. Across cuspFormGamma1OneEquiv, heckeTCuspLevelOne k n agrees with heckeTCompositeGamma0 1 n acting on S_k(Γ₁(1), 1): both have the same Fourier-coefficient divisor-sum formula at every index.

theorem TauCeti.heckeTLevelOne_modularFormGamma1OneEquiv {k : ℤ} (hk : k ≠ 0) (n : ℕ) [NeZero n] (F : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 1)) k) : (heckeTLevelOne k n) ((modularFormGamma1OneEquiv k) F) = (modularFormGamma1OneEquiv k) ↑(((HeckeRing.GL2.heckeRingHomCharSpace k 1) (HeckeRing.GL2.heckeTCompositeGamma0 1 n)) ⟨F, ⋯⟩)

Compatibility of heckeTLevelOne with the composite Γ₀(1) Hecke action at nonzero weight: both operators have the same positive Fourier coefficients, which determine a modular form when k ≠ 0.

theorem TauCeti.commute_heckeTCuspLevelOne (k : ℤ) (m n : ℕ) [NeZero m] [NeZero n] : Commute (heckeTCuspLevelOne k m) (heckeTCuspLevelOne k n)

Level-one Hecke operators on cusp forms commute.

theorem TauCeti.commute_heckeTLevelOne (k : ℤ) (m n : ℕ) [NeZero m] [NeZero n] : Commute (heckeTLevelOne k m) (heckeTLevelOne k n)

Level-one Hecke operators on modular forms commute.

The newform eigenbasis of CuspForm 𝒮ℒ k

noncomputable def TauCeti.levelOneNewformBasis (k : ℤ) : Module.Basis (HeckeRing.GL2.Newform 1 k) ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)

The canonical basis of S_k(SL(2, ℤ)) consisting of normalized Hecke eigenforms, obtained by transporting HeckeRing.GL2.Newform.basis 1 k along cuspFormsNew_one and cuspFormGamma1OneEquiv.

@[simp]

theorem TauCeti.coe_levelOneNewformBasis_apply (k : ℤ) (f : HeckeRing.GL2.Newform 1 k) : ⇑((levelOneNewformBasis k) f) = ⇑f.toCuspForm

At a newform f, the basis vector levelOneNewformBasis k f has the same underlying function on ℍ as f.toCuspForm.

@[simp]

theorem TauCeti.cuspFormGamma1OneEquiv_toCuspForm (k : ℤ) (f : HeckeRing.GL2.Newform 1 k) : (cuspFormGamma1OneEquiv k) f.toCuspForm = (levelOneNewformBasis k) f

cuspFormGamma1OneEquiv carries f.toCuspForm to levelOneNewformBasis k f.

theorem HeckeRing.GL2.Newform.twelve_le_weight {k : ℤ} (f : Newform 1 k) : 12 ≤ k

Every level-one newform has weight k ≥ 12, since S_k(SL(2, ℤ)) = 0 for k < 12.

theorem TauCeti.heckeTCuspLevelOne_levelOneNewformBasis (k : ℤ) (n : ℕ) [NeZero n] (f : HeckeRing.GL2.Newform 1 k) : (heckeTCuspLevelOne k n) ((levelOneNewformBasis k) f) = (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm) • (levelOneNewformBasis k) f

Each basis vector of levelOneNewformBasis k is an eigenform of every heckeTCuspLevelOne, with eigenvalue equal to its n-th Fourier coefficient.

@[simp]

theorem TauCeti.heckeTCuspLevelOne_one (k : ℤ) : heckeTCuspLevelOne k 1 = 1

T₁ is the identity on S_k(SL(2, ℤ)): it fixes each newform, whose first Fourier coefficient is 1.

theorem TauCeti.heckeTCuspLevelOne_prime_pow_add_two (k : ℤ) (p : ℕ) [Fact (Nat.Prime p)] (r : ℕ) : heckeTCuspLevelOne k (p ^ (r + 2)) = heckeTCuspLevelOne k p * heckeTCuspLevelOne k (p ^ (r + 1)) - ↑p ^ (k - 1) • heckeTCuspLevelOne k (p ^ r)

The prime-power recurrence of the level-one Hecke operators: T_{p^{r+2}} = Tₚ T_{p^{r+1}} - p^{k-1} T_{p^r} on S_k(SL(2, ℤ)) for a prime p (Diamond–Shurman Proposition 5.3.1). Both sides act on each newform by the corresponding combination of its Fourier coefficients, which satisfy this recurrence.

theorem TauCeti.trace_heckeTCuspLevelOne (k : ℤ) (n : ℕ) [NeZero n] : (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)) (heckeTCuspLevelOne k n) = ∑ᶠ (f : HeckeRing.GL2.Newform 1 k), (PowerSeries.coeff n) (UpperHalfPlane.qExpansion 1 ⇑f.toCuspForm)

The trace of Tₙ on S_k(SL(2, ℤ)) is the sum of the n-th Fourier coefficients of the level-one newforms.

theorem TauCeti.levelOneNewformBasis_mem_of_forall_prime {k : ℤ} {W : Submodule ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k)} (hW : ∀ (p : Nat.Primes), ∀ g ∈ W, (heckeTCuspLevelOne k ↑p) g ∈ W) {g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k} (hg : g ∈ W) {f : HeckeRing.GL2.Newform 1 k} (hf : ((levelOneNewformBasis k).repr g) f ≠ 0) : (levelOneNewformBasis k) f ∈ W

Prime-Hecke invariant subspaces of S_k(SL(2, ℤ)) contain every newform occurring in their elements. Two distinct level-one newforms differ in their eigenvalue at some prime (strong multiplicity one, Newform.eq_of_forall_prime_eigenvalue_eq), so the joint prime-Hecke weights on levelOneNewformBasis k are injective and Module.Basis.self_mem_of_repr_ne_zero_of_forall clears extra coordinates.

theorem TauCeti.injective_of_heckeTCuspLevelOne_mem_ker {k : ℤ} {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {φ : ℂ →+* R} {L : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k →ₛₗ[φ] M} (hker : ∀ (p : Nat.Primes), ∀ g ∈ L.ker, (heckeTCuspLevelOne k ↑p) g ∈ L.ker) (hbasis : ∀ (f : HeckeRing.GL2.Newform 1 k), L ((levelOneNewformBasis k) f) ≠ 0) : Function.Injective ⇑L

Injectivity criterion on S_k(SL(2, ℤ)) via prime Hecke operators. A semilinear map out of CuspForm 𝒮ℒ k whose kernel is stable under heckeTCuspLevelOne k p for every prime p and that vanishes on no basis vector of levelOneNewformBasis k is injective.

The normalized Eisenstein series as a Hecke eigenform

theorem TauCeti.qExpansion_coeff_one_E_ne_zero {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑(ModularForm.E hk)) ≠ 0

The first Fourier coefficient of ModularForm.E hk at even weight k ≥ 4 is nonzero: all positive coefficients are multiples of it (E_qExpansion_coeff), and a nonzero modular form of nonzero weight cannot have all positive Fourier coefficients equal to zero.

theorem TauCeti.heckeTLevelOne_E {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (n : ℕ) [NeZero n] : (heckeTLevelOne (↑k) n) (ModularForm.E hk) = ↑((ArithmeticFunction.sigma (k - 1)) n) • ModularForm.E hk

The normalized Eisenstein series E_k is a Hecke eigenform with eigenvalue σ_{k-1}(n) at every n ≥ 1 (Serre, A Course in Arithmetic, VII.5.3; Diamond–Shurman, Proposition 5.2.3).

The cusp/Eisenstein decomposition and trace of Tₙ on ModularForm 𝒮ℒ k

theorem TauCeti.isCompl_cuspFormSubmodule_span_E {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) : IsCompl (ModularForm.cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) (ℂ ∙ ModularForm.E hk)

At even weight k ≥ 4, M_k(SL(2, ℤ)) is the internal direct sum of S_k(SL(2, ℤ)) and ℂ · E_k.

theorem TauCeti.trace_heckeTLevelOne {k : ℕ} (hk : 3 ≤ k) (hk2 : Even k) (n : ℕ) [NeZero n] : (LinearMap.trace ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)) (heckeTLevelOne (↑k) n) = (LinearMap.trace ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)) (heckeTCuspLevelOne (↑k) n) + ↑((ArithmeticFunction.sigma (k - 1)) n)

The trace of Tₙ on M_k(SL(2, ℤ)) at even weight k ≥ 4 is the cusp-form trace plus σ_{k-1}(n).