Definitions/Def_FreyPackage_MazurEichlerShimuraFamily.lean

Two conditional predicates are introduced. For M \ge 1 and a natural number p, ModularCurve.EichlerShimuraRelationOn M p asserts: if HeckeInputsAll M holds — that is, for every prime \ell the data HeckeInputsAlong (AlgebraicClosure ℚ) M ℓ (integrality of the two degeneracy maps \alpha,\beta from the base-changed full modular function field of level M into that of level M\ell, existence of principal divisors at level M\ell, finiteness along \alpha, the fundamental identity along \beta and the pushforward norm formula along \alpha) is available, so that the Hecke correspondence operator on J_0(M) = \mathrm{Pic}^0 of the level-M function field over \overline{\mathbb Q} is the intended one rather than 0; and if HeckeOperatorsCommuteBar M holds, i.e. the endomorphisms heckeOperatorBar M ℓ of JZero M commute pairwise — then, with JZero M regarded as a module over \mathbb T = \mathbb Z[T_\ell : \ell \text{ prime}] = MvPolynomial Nat.Primes ℤ via heckeModuleBar M (evaluation of polynomials at the Hecke endomorphisms), the predicate FrobeniusQuadraticConcrete M p holds. The latter unfolds to: for every prime \ell \nmid Mp, every valuation subring A of \overline{\mathbb Q} with \ell in its nonunits, every \sigma \in \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) that is a Frobenius at \ell for A, and every x \in J_0(M) annihilated by some power of p, \sigma^2 x - T_\ell(\sigma x) + \ell x = 0, the Galois action being the arithmetic (coefficientwise) one on the Laurent-series model.

For a Frey package P (nonzero integers a,b,c with a^p+b^p=c^p, p \ge 5 prime, \gcd(a,b)=1, a \equiv 3 \bmod 4, b \equiv 0 \bmod 2) and q \ge 1, FreyPackage.MazurEichlerShimuraFamily P q asserts EichlerShimuraRelationOn (N * q) P.p for every level N \ge 1 with q \nmid N: the congruence relation at the Frey exponent p, uniformly over all levels divisible by q exactly once in this sense.