Definitions/Def_FreyPackage_ExchangeCase.lean

Fix a Frey package P (integers a,b,c with a^p+b^p=c^p, \gcd(a,b)=1, a\equiv 3 \bmod 4, b even, p\ge 5 prime) and a natural number q. The predicate FreyPackage.ExchangeCongruence P q is the integer divisibility p \mid q^2-1; it is decidable, divisibility of integers being decidable.

The other two declarations are the two halves of a case split, each a statement about P and q that is to be assumed or proved as a whole. Both ExchangeCaseLowering P q and MazurPrincipleNewLowering P q assert: for every N>0 with q prime, q\neq 2, q\neq p and q\nmid N, assuming respectively that p \mid q^2-1 (exchange case) or that p \nmid q^2-1 (Mazur case), that the p-torsion of the Frey curve over an algebraic closure of \mathbb{Q} is nontrivial and has no Galois-stable \mathbb{Z}/p-submodules besides \bot and \top, and that the representation P.freyGaloisRep (the Galois action on that p-torsion) is unramified at q in the sense that for every valuation subring A of the algebraic closure in which q is a non-unit the inertia subgroup of A over \mathbb{Q} lies in the kernel, one has: if P.ModularRepOfLevelNewAt (N*q) q holds then P.ModularRepOfLevel N holds.

Here ModularRepOfLevel N means that there exist a weight-2 cusp form f on \Gamma_0(N) which is a normalized eigenform (normalisation and Hecke recursions imposed on its q-expansion coefficients), an integral Weierstrass model W of the Frey curve, and a maximal ideal \mathfrak{m} of the integral closure of \mathbb{Z} in \mathbb{C} containing p, such that for all primes \ell of good reduction for W with \ell \nmid N, \ell \neq p, the coefficient a_\ell(f) is integral and congruent to a_\ell(W) modulo \mathfrak{m}. The variant ModularRepOfLevelNewAt M q requires the same congruence data at level M together with the newness condition a_q(g)^2=1. Thus the conclusion is a congruence between a form of level N and the Frey curve, not an isomorphism of representations.