Definitions/Def_WeierstrassCurve_ThreeFiveSwitchConditioned.lean

This module defines a single predicate, WeierstrassCurve.ThreeFiveSwitchCurveAtThreeConditioned, on a Weierstrass curve W over \mathbb{Z}. It asserts an implication: if the discriminant \Delta(W) is nonzero, if W is a semistable model in the sense that every prime p dividing \Delta(W) fails to divide c_4(W) (IsSemistableModel), and if the mod-5 representation of W is irreducible — meaning, by ModRepIsIrreducible, that the \mathbb{Z}/5-module of 5-torsion points of W base-changed to \overline{\mathbb{Q}} is nontrivial and its only submodules stable under all \mathbb{Q}-automorphisms of \overline{\mathbb{Q}} are \bot and \top — then there exists a further Weierstrass curve W' over \mathbb{Z} with the following properties. First, \Delta(W')\neq 0 and W' is again a semistable model. Second, the mod-3 representation of W' is irreducible in the same sense, and it has a unipotent element (ModRepHasUnipotent): some \sigma \in \mathrm{Aut}_{\mathbb{Q}}(\overline{\mathbb{Q}}) acts on the 3-torsion by an endomorphism \rho(\sigma) with (\rho(\sigma)-1)^2 = 0 and \rho(\sigma) - 1 \neq 0. Third, a conditional clause at 3: if 3 \mid \Delta(W) or 3 \nmid a_3(W), then likewise 3 \mid \Delta(W') or 3 \nmid a_3(W'); here IsGoodPrimeFor \ell means \ell \nmid \Delta, and apOfModel \ell is \#\mathbb{Z}/\ell + 1 minus the number of points of the reduction of the model modulo \ell. Fourth, for every prime \ell \neq 5 at which both W and W' are good, 5 \mid a_\ell(W') - a_\ell(W). The link between W' and W is thus a congruence of Frobenius traces modulo 5 at primes good for both models, not an asserted isomorphism of mod-5 representations; and all the conditions are conditions on the chosen integral models, phrased through \Delta, c_4 and point counts of reductions.