Definitions/Def_FreyPackage_LoweringAt.lean

Three predicates on a Frey package P (a triple a,b,c of nonzero integers with a^p+b^p=c^p for a prime p\ge 5, \gcd(a,b)=1, a\equiv 3 \pmod 4, b even) are defined; each is an implication asserting that a congruence between the mod p representation of the Frey curve and a newform of level divisible by an auxiliary prime can be descended to one of smaller level. They differ from the earlier variants of the same shape only in the conclusion: instead of ModularRepOfLevel, which asserts the existence of a level-N normalised weight-two eigenform on \Gamma_0(N), of some integral model W of P.freyCurve and of a maximal ideal \mathfrak m of the integral closure of \mathbb Z in \mathbb C containing p, with a_\ell(f)\equiv a_\ell(W) \bmod \mathfrak m for all primes \ell\nmid N, \ell\ne p of good reduction, the conclusion here is ModularRepOfLevelAt N, where the model is pinned down to be the fixed integral Weierstrass model freyCurveInt P.

The hypotheses are unchanged. MazurPrincipleNewLoweringAt P q assumes N>0, q prime, q\ne 2, q\ne p, q\nmid N, that p\nmid q^2-1 (the negation of ExchangeCongruence), that the p-torsion of the Frey curve over an algebraic closure of \mathbb Q is nontrivial with no proper nonzero Galois-stable \mathbb Z/p-submodule, that freyGaloisRep kills the inertia subgroups of all valuation subrings lying over q, and ModularRepOfLevelNewAt (N*q) q (a congruent eigenform g of level Nq with a_q(g)^2=1). ExchangeCaseLoweringAt P q is the same with p\mid q^2-1 assumed instead. AtPNewLoweringAt P assumes N_0>0, p\nmid N_0, the same irreducibility, that p divides the p-adic valuation of the discriminant of P.freyCurve, and ModularRepOfLevelNewAt (N₀ * P.p) P.p, concluding ModularRepOfLevelAt N₀. A local decidable-equality instance on \overline{\mathbb Q} is also provided.