Full Hecke eigenforms #
A full Hecke eigenform is a nonzero cusp form of nebentypus χ that is an eigenvector for
T_n at every positive index n, including the primes dividing the level. This is the
unqualified notion of eigenform: EigenformAwayFromLevel remains the weaker object carrying
only the good-index eigenrelations.
The prime operators determine the full eigensystem. At a good prime the prime-power blocks
satisfy the usual Hecke recurrence; at a prime dividing the level they are powers of U_p = T_p.
The coprime multiplication law then combines the prime-power blocks, including a mixture of good
and bad primes.
Main declarations #
HeckeRing.GL2.Eigenform: a nonzero cusp form with nebentypus and eigenvalues at every positive index.HeckeRing.GL2.Eigenform.ofForallPrime: construct a full eigenform from eigenrelations at every prime.HeckeRing.GL2.EigenformAwayFromLevel.toEigenform: upgrade a good Hecke eigenform once the missing bad-prime eigenrelations are supplied.HeckeRing.GL2.Eigenform.qExpansion_coeff_eq_eigenvalue_mul_coeff_one: the coefficient at every positive index is its eigenvalue times the first coefficient.HeckeRing.GL2.Eigenform.eigenvalue_mul,HeckeRing.GL2.Eigenform.eigenvalue_prime_pow_add_two: the eigenvalues are multiplicative at coprime indices and satisfy the Hecke recurrence along the powers of every prime, with the nebentypus zero-extended to the primes dividing the level.HeckeRing.GL2.Eigenform.qExpansion_coeff_mul,HeckeRing.GL2.Eigenform.qExpansion_coeff_prime_pow_add_two: the same identities for the coefficients of a normalised eigenform, conditions (2) and (3) of Diamond–Shurman's Proposition 5.8.5 at every index.HeckeRing.GL2.Eigenform.qExpansion_coeff_mem_of_forall_prime: by these identities, every coefficient of a normalised eigenform lies in each subring ofℂcontaining the coefficients at the primes and the scalarsχ(p) p^{k−1}of the recurrence.
Provenance #
The bundled layout specializes EigenformAwayFromLevel, whose shape is adapted from AINTLIB's
LeanModularForms/HeckeRIngs/GL2/Newforms/Basic.lean (Chris Birkbeck, commit
2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0). The eigencondition here is redesigned
over Tau Ceti's positive-index heckeTCompositeGamma0 API and includes the bad indices; the
prime-assembly proof composes Tau Ceti's good-prime recurrence, bad-prime power identity, and
coprime product formula.
References #
- F. Diamond and J. Shurman, A first course in modular forms, Definition 5.8.1 and Proposition 5.8.5.
- T. Miyake, Modular forms, §4.5.
A full Hecke eigenform. This is a nonzero cusp form in a fixed nebentypus space together
with its eigenvalue at every positive index. In contrast with EigenformAwayFromLevel, no
coprimality condition excludes the primes dividing the level.
- toFun : UpperHalfPlane → ℂ
- slash_action_eq' (γ : GL (Fin 2) ℝ) : γ ∈ Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N) → SlashAction.map k γ self.toFun = self.toFun
- holo' : MDiff ⇑self.toSlashInvariantForm
- zero_at_cusps' {c : OnePoint ℝ} (hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma1 N))) : c.IsZeroAt self.toFun k
The nebentypus character.
The form transforms under the diamond operators by
χ.The eigenvalue at a positive index.
- isEigen (n : ℕ+) : ((heckeRingHomCuspCharSpace k self.χ) (heckeTCompositeGamma0 N ↑n)) ⟨self.toCuspForm, ⋯⟩ = self.eigenvalue n • ⟨self.toCuspForm, ⋯⟩
The Hecke element
T_nacts on the form byeigenvalue n. An eigenform is nonzero.
Instances For
A full eigenform is, in particular, an eigenform away from the level.
Equations
- f.toEigenformAwayFromLevel = { toCuspForm := f.toCuspForm, χ := f.χ, mem_charSpace := ⋯, eigenvalue := fun (n : ℕ+) (x : (↑n).Coprime N) => f.eigenvalue n, isEigen := ⋯, ne_zero := ⋯ }
Instances For
Extensionality. A full eigenform is determined by its underlying cusp form. The form determines the nebentypus, and nonvanishing makes every eigenvalue unique.
Construct a full eigenform from its prime eigenrelations. Eigen-ness at every prime spreads through the prime-power recurrences and coprime multiplication to every positive index.
Equations
Instances For
Every positive-index coefficient of a full eigenform is its eigenvalue times a₁.
The first coefficient of T_n f is a_n(f), at good and bad indices alike.
The eigenvalue system #
The eigenvalue at 1 is 1: the Hecke element at index 1 is the identity.
Multiplicativity on coprime indices: λ_{mn} = λ_m λ_n, the image of the coprime
multiplication rule heckeTCompositeGamma0_mul_of_coprime. Unlike
EigenformAwayFromLevel.eigenvalue_mul, the indices may share primes with the level.
The recurrence along the powers of a prime:
λ_{p^{r+2}} = λ_p λ_{p^{r+1}} − χ(p) p^{k−1} λ_{p^r}, with χ(p) read through Mathlib's
zero-extension MulChar.ofUnitHom. At a good prime this is
EigenformAwayFromLevel.eigenvalue_prime_pow_add_two; at a prime dividing the level the
character term vanishes and the identity is T_{p^{r+2}} = T_p T_{p^{r+1}}, from
T_{p^v} = T_p^v (heckeTCompositeGamma0_prime_pow_of_not_coprime).
The Fourier coefficients of a normalised eigenform #
With a₁ = 1 the coefficients are the eigenvalues, so they satisfy conditions (2) and (3) of
Diamond–Shurman's Proposition 5.8.5 at every index, good or bad. These are exactly the hypotheses
of the Euler product.
The coefficients of a normalised full eigenform are its eigenvalues: a_n(f) = λ_n at
every positive index n, when a_1(f) = 1.
Multiplicativity of the coefficients of a normalised full eigenform: a_{mn} = a_m a_n
for all coprime m, n (Diamond–Shurman Proposition 5.8.5 (3)).
The prime-power recurrence for the coefficients of a normalised full eigenform:
a_{p^{r+2}} = a_p a_{p^{r+1}} − χ(p) p^{k−1} a_{p^r} at every prime p, with χ(p) = 0 for
p ∣ N (Diamond–Shurman Proposition 5.8.5 (2)).
The coefficients of a normalised full eigenform lie in every subring containing the prime
data of its Hecke recurrence. If a₁ = 1 and a subring of ℂ contains a_p and
χ(p) p^{k−1} for every prime p, with χ(p) = 0 for p ∣ N, then it contains every
coefficient a_n.
Upgrade a good Hecke eigenform to a full eigenform from the bad-prime equations. The
input supplies precisely what EigenformAwayFromLevel omits: at every prime dividing the level,
the classical operator U_p = T_p acts by a scalar.
Equations
- f.toEigenform hbad = HeckeRing.GL2.Eigenform.ofForallPrime ⋯ ⋯ ⋯