Building a good Hecke eigenform from the prime eigenvalues

EigenformAwayFromLevel bundles a cusp form with an eigenvalue at every index coprime to the level. Eigen-ness at those indices is already determined by the primes (exists_smul_heckeTCompositeGamma0_of_forall_prime_of_coprime), so a nonzero cusp form of nebentypus χ that is an eigenvector of the Hecke-ring generator at every prime p ∤ N bundles into one. That is the shape in which eigenforms are produced: a coefficient recurrence, a diagonalisation or a spectral argument gives the eigenvector equation one prime at a time.

Main results

• HeckeRing.GL2.EigenformAwayFromLevel.ofForallPrime: the good Hecke eigenform carried by a nonzero cusp form eigen at every prime away from the level.

References

• F. Diamond and J. Shurman, A first course in modular forms, §5.8.
• T. Miyake, Modular forms, §4.5.

noncomputable def HeckeRing.GL2.EigenformAwayFromLevel.ofForallPrime {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hχ : f ∈ cuspFormCharSpace k χ) (hf : f ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ⟨f, hχ⟩ = c • ⟨f, hχ⟩) : EigenformAwayFromLevel N k

A nonzero cusp form of nebentypus χ, eigen at every good prime, is a good Hecke eigenform. Its eigenvalue at a good index is the scalar by which the Hecke ring acts there, supplied by exists_smul_heckeTCompositeGamma0_of_forall_prime_of_coprime.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HeckeRing.GL2.EigenformAwayFromLevel.ofForallPrime_toCuspForm {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hχ : f ∈ cuspFormCharSpace k χ) (hf : f ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ⟨f, hχ⟩ = c • ⟨f, hχ⟩) : (ofForallPrime hχ hf h).toCuspForm = f

The underlying cusp form of ofForallPrime is the form supplied to the constructor.

@[simp]

theorem HeckeRing.GL2.EigenformAwayFromLevel.ofForallPrime_χ {N : ℕ} [NeZero N] {k : ℤ} {χ : (ZMod N)ˣ →* ℂˣ} {f : CuspForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N)) k} (hχ : f ∈ cuspFormCharSpace k χ) (hf : f ≠ 0) (h : ∀ (p : ℕ), Nat.Prime p → p.Coprime N → ∃ (c : ℂ), ((heckeRingHomCuspCharSpace k χ) (heckeTGeneratorGamma0 N p)) ⟨f, hχ⟩ = c • ⟨f, hχ⟩) : (ofForallPrime hχ hf h).χ = χ

The nebentypus of ofForallPrime is the character supplied to the constructor.