Definitions/Def_CuspForm_EigenformCoefficientRing.lean

Throughout, M is a natural number and g a cusp form of weight 2 on \Gamma_0(M); no Hecke-eigenform hypothesis is imposed, so the names below refer to the coefficients of g alone. Fourier coefficients are taken in the project's sense, a_n(g) = the n-th coefficient of the q-expansion of g of width 1. The predicate PrimeCoeffsIntegral g asserts that for every prime \ell there is an element of integralClosure ℤ ℂ, the ring \overline{\mathbb Z} of algebraic integers inside \mathbb C, whose image in \mathbb C is a_\ell(g); that is, each prime-indexed coefficient of g is an algebraic integer. Under a hypothesis hint of this form, eigenLift hint ℓ is a witnessing element of \overline{\mathbb Z}, and eigenLift_coe records that its image in \mathbb C is a_\ell(g); since \overline{\mathbb Z} is a subring of \mathbb C, this element is in fact the unique algebraic integer with that image. The coefficient ring eigenCoeffRing hint is the \mathbb Z-subalgebra of \overline{\mathbb Z} generated by the range of these lifts, i.e. R_g = \mathbb Z[a_\ell(g) : \ell \text{ prime}]; eigenLift_mem_eigenCoeffRing states that each lift lies in it. Given in addition an ideal \mathfrak m_w of \overline{\mathbb Z} (no maximality or primality is assumed), eigenResidueIdeal is its contraction \lambda = \mathfrak m_w \cap R_g along the inclusion R_g \hookrightarrow \overline{\mathbb Z}, EigenResidueRing abbreviates the quotient ring R_g/\lambda, and eigenSystemMod is the resulting system of reduced coefficients, the map sending a prime \ell to the class of a_\ell(g) in R_g/\lambda. No finiteness, field or characteristic properties of R_g/\lambda are asserted at this stage.