Definitions/Def_WeierstrassCurve_ModularityProps.lean

Five predicates on integral Weierstrass models are introduced, all phrased for a chosen model W over \mathbb{Z} rather than for an isomorphism class over \mathbb{Q}.

ModRepHasUnipotent W n asserts the existence of a \mathbb{Q}-algebra automorphism \sigma of \overline{\mathbb{Q}} = AlgebraicClosure ℚ whose induced \mathbb{Z}/n-linear endomorphism u = \rho(\sigma) of the n-torsion submodule of the group of affine points of W base-changed to \overline{\mathbb{Q}} (the endomorphism supplied by galoisRepModuleEnd) satisfies (u-1)(u-1) = 0 together with u - 1 \neq 0: some Galois element acts unipotently but non-trivially.

The remaining four are named statements to be cited as hypotheses: LanglandsTunnellWeightTwo and ModularityLiftingAt p are closed propositions (the latter depending only on a prime), while ModThreeOrFiveIrreducible W and ThreeFiveSwitchCurve W depend on the model W. LanglandsTunnellWeightTwo says: every W with \Delta \neq 0 which is semistable in the project's sense (no prime dividing \Delta divides c_4) and has irreducible mod-3 torsion representation is residually modular at 3, meaning that for some level M > 0 there is a normalised weight-two eigenform on \Gamma_0(M) and a maximal ideal \mathfrak{m} of the integral closure of \mathbb{Z} in \mathbb{C} containing 3 with a_\ell(f) \equiv a_\ell(W) \pmod{\mathfrak{m}} for all primes \ell \nmid \Delta, \ell \nmid M, \ell \neq 3, where a_\ell(W) is computed as \ell + 1 - \#W(\mathbb{F}_\ell) for the reduction of the model. ModThreeOrFiveIrreducible W says that a semistable W with \Delta \neq 0 has irreducible mod-3 or mod-5 torsion representation. ThreeFiveSwitchCurve W says that for such W with irreducible mod-5 representation there is a second model W' with \Delta' \neq 0, semistable, mod-3 irreducible, possessing a non-trivial unipotent in its mod-3 representation, satisfying 3 \mid \Delta' or 3 \nmid a_3(W'), and congruent to W in the sense that 5 \mid a_\ell(W') - a_\ell(W) for every prime \ell \neq 5 good for both. ModularityLiftingAt p says that semistability, \Delta \neq 0, mod-p irreducibility and residual modularity at p imply that W is modular of some level N > 0 divisible by every prime dividing \Delta. A local instance equips \overline{\mathbb{Q}} with classical decidable equality, as required by the torsion-representation definitions.