Definitions/Def_FreyPackage_EigenformResidualAttachment.lean

The module defines a single predicate, EigenformResidualAttachmentAt P M, on a Frey package P=(a,b,c,p) and a natural number M. It asserts: for every weight-2 cusp form g on \Gamma_0(M) which is a normalised eigenform in the project's sense (first q-coefficient 1, multiplicativity of q-coefficients at coprime indices, and the two prime-power recursions according to whether the prime divides the level), and for every maximal ideal \mathfrak m of \mathrm{integralClosure}\,\mathbb Z\,\mathbb C (the ring of all algebraic integers in \mathbb C) containing the image of p, there exist: a field K carrying a \mathbb Z/p-algebra structure, a K-vector space V with a representation \rho of \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q), realised as the group of \mathbb Q-algebra automorphisms of AlgebraicClosure ℚ, a ring homomorphism \psi from the algebraic integers to K, and a number field F, Galois over \mathbb Q and embedded in \overline{\mathbb Q} compatibly over \mathbb Q, subject to four conditions: (i) \mathfrak m\subseteq\ker\psi, so \psi is a residue map at \mathfrak m; (ii) \dim_K V=2; (iii) the kernel of the restriction homomorphism \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q)\to\mathrm{Gal}(F/\mathbb Q) lies in the intersection of \ker\rho with the kernel of the action of \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) on the p-torsion of the Frey curve over \overline{\mathbb Q} (the monoid homomorphism galoisRepModuleEnd), i.e. both representations factor through \mathrm{Gal}(F/\mathbb Q); (iv) for every prime \ell\nmid M with \ell\neq p, every valuation subring A of \overline{\mathbb Q} in which \ell is a non-unit, and every \tau that is a Frobenius at \ell for A (in the decomposition subgroup, acting as x\mapsto x^{\ell} on the residue field of A), one has \mathrm{tr}\,\rho(\tau)=\psi(a) for some algebraic integer a whose complex value is the \ell-th q-coefficient of g, and \det\rho(\tau)=\ell in K.

Note what is not required: no irreducibility of \rho, and no congruence relating \rho to the mod-p representation of the Frey curve — condition (iii) only forces the two to be trivial on a common open normal subgroup, so that both are determined by their values on \mathrm{Gal}(F/\mathbb Q). The module also installs a classical decidable-equality instance on AlgebraicClosure ℚ, needed for the torsion-module machinery.