Documentation

TauCeti.NumberTheory.ModularForms.Newforms.Hecke.Stability

Hecke stability of the old and new subspaces #

The old subspace of S_k(Γ₁(N)) is stable under the Hecke operator Tₚ at every prime p, and the new subspace is stable under Tₚ for p coprime to the level.

The old subspace is generated by the level-raises V_d g of cusp forms g of proper divisor level M, so stability is exactly the statement that Tₚ carries each such generator back into the subspace; the elimination rule cuspFormsOld_le turns that generator-wise statement into the stability of the whole subspace. For p coprime to N the generator statement is heckeTCuspNat_levelRaise: Tₚ commutes with V_d. For p ∣ N the operator Tₚ at level N is Uₚ, reading off the coefficients a_{p m}, and it no longer commutes with V_d; instead Tₚ (V_d g) is computed on q-expansions (HeckeSlash/Degeneracy.lean) as V_{d/p} g when p ∣ d, as V_d (Tₚ g) when p ∤ d and p ∣ M, and as V_d (Tₚ g) - p ^ (k - 1) • V_{d p} (⟨p⟩ g) when p ∤ d M, each an old form.

This mirrors the diamond half, diamondOpCusp_mem_cuspFormsOld, which is proved from CuspForm.diamondOpCusp_levelRaise. Together they say the old subspace is stable under every Tₚ and every diamond operator.

The new subspace is the Petersson-orthogonal complement of the old subspace. For p coprime to N its stability follows from the old-space stability, because the Petersson adjoint of Tₚ is ⟨p⟩⁻¹ Tₚ there. It is the invariant-subspace input for restricting the simultaneous good-Hecke diagonalization to the newspace. The stability of both old and new subspaces under every Hecke operator is Diamond–Shurman, A First Course in Modular Forms, Proposition 5.6.2; at p ∣ N the old-space half is proved here. The new-space half at p ∣ N does not follow the same way, since the adjoint of Uₚ is not a multiple of Uₚ; it is proved from the newform basis in TauCeti.NumberTheory.ModularForms.Newforms.BadPrime.Stability.

Both stability statements also hold for the Hecke-ring generator heckeTGeneratorGamma0 N p, acting on a character space — the form eigenform arguments need, since eigen-ness of an EigenformAwayFromLevel is stated for heckeRingHomCuspCharSpace rather than for heckeTCuspNat. No separate argument is required: at a prime the two operators agree on S_k(N, χ) (HeckeRing.GL2.coe_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0). Since every T_n in the ring is a polynomial in the prime generators and the scalar cosets (HeckeRing.GL2.heckeRingHomCuspCharSpace_heckeTCompositeGamma0_mem_of_forall_prime_dvd), the old part of S_k(N, χ) is moreover stable under every T_n, the indices sharing a factor with the level included.

Main results #

The old subspace #

source
theorem TauCeti.heckeTCuspNat_mem_cuspFormsOld {k : ℤ} {N p : ℕ} [NeZero N] (hp : Nat.Prime p) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsOld N k) :
(HeckeRing.GL2.heckeTCuspNat k p) f ∈ cuspFormsOld N k

The old subspace is Hecke-stable at every prime p: Tₚ maps S_k(Γ₁(N))ᵒˡᵈ into itself, whether or not p divides the level. At p ∣ N this is the old-space half of Diamond–Shurman's Proposition 5.6.2 for the operator Uₚ = Tₚ.

source
theorem TauCeti.coe_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0_mem_cuspFormsOld {k : ℤ} {N p : ℕ} [NeZero N] {χ : (ZMod N)ˣ →* ℂˣ} (hp : Nat.Prime p) {F : ↥(cuspFormCharSpace k χ)} (hF : ↑F ∈ cuspFormsOld N k) :
↑(((HeckeRing.GL2.heckeRingHomCuspCharSpace k χ) (HeckeRing.GL2.heckeTGeneratorGamma0 N p)) F) ∈ cuspFormsOld N k

The old part of S_k(N, χ) is stable under the Hecke-ring generator at a prime, in the form eigenform arguments need it: heckeTGeneratorGamma0 N p acting on the character space carries an old form to an old form. At a prime that action is the classical Tₚ (HeckeRing.GL2.coe_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0), so this is heckeTCuspNat_mem_cuspFormsOld read through that identification.

source
theorem TauCeti.cuspFormsOld_comap_map_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0_le {N p : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) (hp : Nat.Prime p) (k : ℤ) :
Submodule.map ((HeckeRing.GL2.heckeRingHomCuspCharSpace k χ) (HeckeRing.GL2.heckeTGeneratorGamma0 N p)) (Submodule.comap (cuspFormCharSpace k χ).subtype (cuspFormsOld N k)) ≤ Submodule.comap (cuspFormCharSpace k χ).subtype (cuspFormsOld N k)

The same stability in Submodule.map form: the Hecke-ring generator at a prime carries the preimage of cuspFormsOld in the character space into itself. The counterpart of cuspFormsOld_map_heckeTCuspNat_le for that generator; the old subspace is pulled back along the inclusion because the action is on cuspFormCharSpace, not on all of S_k(Γ₁(N)).

source
theorem TauCeti.coe_heckeRingHomCuspCharSpace_heckeTCompositeGamma0_mem_cuspFormsOld {k : ℤ} {N : ℕ} [NeZero N] {χ : (ZMod N)ˣ →* ℂˣ} (n : ℕ) {F : ↥(cuspFormCharSpace k χ)} (hF : ↑F ∈ cuspFormsOld N k) :
↑(((HeckeRing.GL2.heckeRingHomCuspCharSpace k χ) (HeckeRing.GL2.heckeTCompositeGamma0 N n)) F) ∈ cuspFormsOld N k

The old part of S_k(N, χ) is stable under every Hecke operator T_n, the composite element heckeTCompositeGamma0 N n of the Γ₀(N) Hecke ring acting on S_k(N, χ), whether or not n shares a factor with the level. This is the old-space half of Diamond–Shurman's Proposition 5.6.2 for the operators T_n; it follows from the prime case coe_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0_mem_cuspFormsOld.

source
theorem TauCeti.cuspFormsOld_comap_map_heckeRingHomCuspCharSpace_heckeTCompositeGamma0_le {N : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) (n : ℕ) (k : ℤ) :
Submodule.map ((HeckeRing.GL2.heckeRingHomCuspCharSpace k χ) (HeckeRing.GL2.heckeTCompositeGamma0 N n)) (Submodule.comap (cuspFormCharSpace k χ).subtype (cuspFormsOld N k)) ≤ Submodule.comap (cuspFormCharSpace k χ).subtype (cuspFormsOld N k)

The old part of S_k(N, χ) is stable under every T_n, in Submodule.map form.

source
theorem TauCeti.cuspFormsOld_map_heckeTCuspNat_le {N p : ℕ} [NeZero N] (hp : Nat.Prime p) (k : ℤ) :
Submodule.map (HeckeRing.GL2.heckeTCuspNat k p) (cuspFormsOld N k) ≤ cuspFormsOld N k

The old subspace is Hecke-stable at every prime, in the Submodule.map form.

The new subspace #

source
theorem TauCeti.heckeTCuspNat_mem_cuspFormsNew_of_coprime {k : ℤ} {N p : ℕ} [NeZero N] (hp : Nat.Prime p) (hpN : p.Coprime N) {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hf : f ∈ cuspFormsNew N k) :
(HeckeRing.GL2.heckeTCuspNat k p) f ∈ cuspFormsNew N k

The new subspace is Hecke-stable at a prime p coprime to the level: Tₚ maps S_k(Γ₁(N))ⁿᵉᵂ into itself.

source
theorem TauCeti.coe_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0_mem_cuspFormsNew {k : ℤ} {N p : ℕ} [NeZero N] {χ : (ZMod N)ˣ →* ℂˣ} (hp : Nat.Prime p) (hpN : p.Coprime N) {F : ↥(cuspFormCharSpace k χ)} (hF : ↑F ∈ cuspFormsNew N k) :
↑(((HeckeRing.GL2.heckeRingHomCuspCharSpace k χ) (HeckeRing.GL2.heckeTGeneratorGamma0 N p)) F) ∈ cuspFormsNew N k

The new part of S_k(N, χ) is stable under the Hecke-ring generator at a good prime. This is the fixed-nebentypus form used to restrict the simultaneous good-Hecke diagonalization to the newspace.

source
theorem TauCeti.cuspFormsNew_comap_map_heckeRingHomCuspCharSpace_heckeTGeneratorGamma0_le {N p : ℕ} [NeZero N] (χ : (ZMod N)ˣ →* ℂˣ) (hp : Nat.Prime p) (hpN : p.Coprime N) (k : ℤ) :
Submodule.map ((HeckeRing.GL2.heckeRingHomCuspCharSpace k χ) (HeckeRing.GL2.heckeTGeneratorGamma0 N p)) (Submodule.comap (cuspFormCharSpace k χ).subtype (cuspFormsNew N k)) ≤ Submodule.comap (cuspFormCharSpace k χ).subtype (cuspFormsNew N k)

The fixed-nebentypus newspace is stable under a good prime Hecke generator, in Submodule.map form. The newspace is pulled back along the inclusion because the Hecke-ring action is on cuspFormCharSpace, not on all of S_k(Γ₁(N)).

source
theorem TauCeti.cuspFormsNew_map_heckeTCuspNat_le_of_coprime {N p : ℕ} [NeZero N] (hp : Nat.Prime p) (hpN : p.Coprime N) (k : ℤ) :
Submodule.map (HeckeRing.GL2.heckeTCuspNat k p) (cuspFormsNew N k) ≤ cuspFormsNew N k

The new subspace is Hecke-stable at a prime coprime to the level, in the Submodule.map form.