Definitions/Def_WeierstrassCurve_ModularityLiftingConductor.lean

Three propositions about integral Weierstrass models are named here. First, IsModularModelOfExactConductorLevel W (an abbreviation for Mlc1IsModularModelOfExactConductorLevel) asserts the existence of a natural number N > 0 that is squarefree, whose prime divisors are exactly the primes q with q \mid \Delta_W (the equivalence q \mid N \iff q \mid \Delta_W being required for every prime q), and such that W.IsModularModelOfLevel N holds: there is a cusp form f of weight 2 for \Gamma_0(N) whose q-expansion coefficients satisfy the normalised-eigenform recursions (first coefficient 1, multiplicativity at coprime indices, and the two prime-power recursions according as the prime divides N or not), with a_p(f) = a_p(W) for every prime p with p \nmid \Delta_W and p \nmid N; here a_p(W) is p + 1 minus the number of points of the reduction of the chosen model modulo p. Second, ModularityLiftingAtConductor p (an abbreviation for Mlc1ModularityLiftingAtConductor) says that every W over \mathbb{Z} with \Delta_W \neq 0, with q \nmid c_4(W) for each prime q \mid \Delta_W, with irreducible mod-p representation in the sense of ModRepIsIrreducible (the p-torsion of the base change of W to \overline{\mathbb{Q}} is nontrivial and its only Galois-stable \mathbb{Z}/p-submodules are \bot and \top), and residually modular at p in the sense of IsResiduallyModular (a normalised eigenform of weight 2 and some positive level M whose coefficients at primes \ell \neq p good for W and not dividing M are congruent to a_\ell(W) modulo a maximal ideal of \overline{\mathbb{Z}} \subset \mathbb{C} containing p), satisfies the exact-conductor-level conclusion above. Third, ModularityLiftingAtConductorOrdinary p is the same implication with the extra hypothesis p \mid \Delta_W or p \nmid a_p(W). All three are conditions on a chosen integral model, and residual modularity is a congruence of coefficients rather than an isomorphism of representations. A classical decidable-equality instance on \overline{\mathbb{Q}} is also provided.