Definitions/Def_ModularCurve_EigenformIdeal.lean

Throughout, the Hecke algebra is taken to be the free commutative ring HeckeAlg =\mathbb{Z}[T_\ell : \ell \text{ prime}] (a multivariate polynomial ring indexed by Nat.Primes, with T_\ell = heckeGen \ell the corresponding variable), and for a family of elements a_\ell of a commutative ring eigenIdeal a is the kernel of the evaluation homomorphism T_\ell \mapsto a_\ell. The first definition, ModularCurve.IsEigenformIdeal N 𝔪, asserts that an ideal \mathfrak m \subseteq \mathbb{Z}[T_\ell] arises from a normalised weight-2 eigenform on \Gamma_0(N) reduced to a finite field: there exist a cusp form f of weight 2 for CongruenceSubgroup.Gamma0 N, a proof that f satisfies CuspForm.IsNormalizedEigenform (a structure whose fields are identities among the q-expansion coefficients a_n(f) = qCoeff f n: a_1 = 1, multiplicativity a_{mn} = a_m a_n for coprime m,n, the recursion a_{p^{r+2}} = a_p a_{p^{r+1}} - p\,a_{p^r} for p \nmid N and a_{p^{r+2}} = a_p a_{p^{r+1}} for p \mid N — so the eigenform condition is formulated purely through coefficients, not through Hecke operators), 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 the eigenvalue ideal of the system \ell \mapsto \varphi(a_\ell(f)). The subring \mathcal O and the map \varphi are part of the existential data; no comparison between \mathbb{Z}[T_\ell] and the Hecke algebra acting on S_2(\Gamma_0(N)) is asserted.

The remaining two declarations instantiate generic predicates with this notion of eigenform ideal. EigenformSupportAt N p J, for an abelian group J with a HeckeAlg-module structure, says: every ideal \mathfrak m which is an eigenform ideal of level N and contains p has nonzero \mathfrak m-torsion in J (the submodule annihilated by all of \mathfrak m is not \bot). EichlerShimuraDataAt N p J, for a field extension L/K and J carrying both a HeckeAlg-module structure and an action of L \simeq_{\mathrm{alg}[K]} L, is the bundled conjunction of three clauses: (i) for every prime \ell \nmid Np, every valuation subring A of L with \ell a nonunit of A, every \sigma in the inertia subgroup of A over K and every p-power-torsion x \in J, one has \sigma \cdot x = x; (ii) for such \ell and A and every \sigma that is a Frobenius at \ell for A (in the decomposition group and inducing x \mapsto x^\ell on the residue field), the Eichler–Shimura relation \sigma^2 x - T_\ell \cdot (\sigma x) + \ell\, x = 0 holds for all p-power-torsion x; (iii) EigenformSupportAt N p J. This is the reduced bundle: the determinant clause on Frobenius and the multiplicity-one conditions available in the same family of definitions are not among its fields.