Definitions/Def_ModularCurve_TwoNewEigenformIdeal.lean

Both notions are phrased over the project's abstract Hecke algebra HeckeAlg, the polynomial ring \mathbb{Z}[X_\ell : \ell \text{ prime}] on generators indexed by the primes, and use eigenIdeal a, the kernel of the \mathbb{Z}-algebra map \mathrm{aeval}\,a sending X_\ell \mapsto a_\ell.

IsTwoNewEigenformIdeal M q q' 𝔪 asserts the existence of a weight-two cusp form f for \Gamma_0(M) together with: a proof that f is a normalised eigenform in the project's sense (first q-expansion coefficient 1, multiplicativity of the coefficients on coprime indices, and the two prime-power recursions a_{p^{r+2}} = a_p a_{p^{r+1}} - p\,a_{p^r} for p \nmid M and a_{p^{r+2}} = a_p a_{p^{r+1}} for p \mid M); proofs that f is new at q and at q', where IsNewAt is the condition a_q^2 = 1 on the relevant coefficient; a finite field k; a subring \mathcal{O} \subseteq \mathbb{C} containing a_\ell(f) for every prime \ell; and a ring homomorphism \varphi : \mathcal{O} \to k; such that \mathfrak{m} is exactly the kernel of the map X_\ell \mapsto \varphi(a_\ell(f)). Thus \mathfrak{m} is the ideal cutting out a residual eigensystem attached to such an f, with the residue field and the reduction map existentially quantified rather than fixed.

TwoNewEigensystemsFactor M q q' Y, for an abelian group Y with a HeckeAlg-module structure, asserts that for every normalised weight-two eigenform f of level \Gamma_0(M) with a_q^2 = 1 and a_{q'}^2 = 1, the annihilator of Y in HeckeAlg is contained in the kernel of X_\ell \mapsto a_\ell(f) \in \mathbb{C}. Equivalently, every polynomial Hecke relation holding on Y also holds on each such complex eigensystem, so that each of these eigensystems factors through the image of HeckeAlg in \mathrm{End}(Y).