Definitions/Def_FreyPackage_EigenformRealizationSupplyField.lean

Fix a Frey package P (integers a,b,c and a prime p\ge 5 with a^p+b^p=c^p, \gcd(a,b)=1, a\equiv 3 \bmod 4, b even) and a level M. ESMasterAttachmentSupplyField P M J is a predicate on an abstract carrier J that is an abelian group, a module over the project's Hecke algebra HeckeAlg (the polynomial ring \mathbb{Z}[T_\ell : \ell \text{ prime}], with heckeGen the variable at \ell), and is equipped with an action of \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), realised as \overline{\mathbb{Q}}-algebra automorphisms of AlgebraicClosure ℚ. No compatibility between the Hecke and Galois actions is assumed. It asserts: for every weight-2 cusp form g on \Gamma_0(M) satisfying the project's IsNormalizedEigenform (first q-coefficient 1, multiplicativity at coprime indices, and the usual prime-power recursions, with or without the p\mid N Euler factor), and for every maximal ideal \mathfrak{m} of the algebraic integers \overline{\mathbb{Z}} = integralClosure ℤ ℂ containing p, there exist a field k, a ring homomorphism \varphi: HeckeAlg \to k, a k-vector space V, a function \pi : J \to V, a homomorphism \rho from the Galois group to \mathrm{GL}_k(V), a ring homomorphism \psi : \overline{\mathbb{Z}} \to k, and a Galois number field F embedded in \overline{\mathbb{Q}} over \mathbb{Q}, such that: p = 0 in k; (k,\varphi,V,\pi,\rho) is an IsResidualRealization of J at p, i.e. \dim_k V = 2 and \pi is additive, Galois-equivariant via \rho and Hecke-semilinear via \varphi on the p-torsion \{x : p\cdot x = 0\}, whose image spans V; \det \rho(\sigma) = \ell in k for every Frobenius \sigma at a place over any prime \ell \nmid Mp; \mathfrak{m} \subseteq \ker\psi; for each prime \ell \nmid Mp the \ell-th q-coefficient of g is an algebraic integer a with \varphi(T_\ell) = \psi(a); and the kernel of restriction \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) \to \mathrm{Gal}(F/\mathbb{Q}) lies in \ker\rho and in the kernel of the P.p-torsion representation of the Frey curve, so both factor through \mathrm{Gal}(F/\mathbb{Q}). The conjunct p = 0 in k follows from the other clauses but is recorded. EigenformRealizationSupplyFieldAt P M is this predicate for J = JZero M, the degree-zero divisor class group of the base-changed modular function field of level M, with its Hecke module structure taken as an instance hypothesis; the accompanying lemma is the definitional unfolding.