Definitions/Def_RibetLevelLowering_CharacterGroupApparatusV2.lean

Three predicates on a Frey package P (with prime exponent p\ge 5), plus a variant of the residual modularity predicate pinned to a fixed integral model.

ModularRepOfLevelAt P N asserts the existence of a weight-2 cusp form f for \Gamma_0(N) and a maximal ideal \mathfrak m of the integral closure of \mathbb Z in \mathbb C such that f is a normalised eigenform (normalised first q-coefficient, multiplicativity on coprime indices, and the two Hecke recursions at prime powers according as the prime divides N or not), p\in\mathfrak m, and for every prime \ell with \ell\nmid\Delta(\mathtt{freyCurveInt}\,P), \ell\nmid N, \ell\ne p, there is an algebraic integer a with a=a_\ell(f) in \mathbb C and a\equiv \#\mathbb F_\ell+1-\#(\mathtt{freyCurveInt}\,P\bmod\ell)\pmod{\mathfrak m}. This differs from ModularRepOfLevel in that the integral Weierstrass model is the explicit Frey model freyCurveInt P rather than an existentially quantified integral model of P.freyCurve.

CharacterGroupApparatus P q asserts: for all N>0 and all primes q,q' with q'\ne q and q,q'\nmid N, if P is residually modular of level Nqq' by a form that is new at q' in the sense a_{q'}^2=1, then there are a field k and an exchange datum d over k — finite-dimensional k-spaces X_p,Y_q,L_p,Y_p,L_q, maps f:Y_q\to L_p, g:L_p\to X_p with g surjective and \ker g\subseteq\operatorname{im}f, and integers \lambda>0,\mu with \dim Y_p=2\mu, \dim L_p=2\lambda, \dim Y_q,\dim X_p\le\mu, \dim L_q\le\lambda — such that failure of residual modularity at level Nq' implies \dim Y_p=\dim L_q. The existential quantifier precedes this implication. CharacterGroupApparatusAt is the same with ModularRepOfLevelAt as the trigger, and CharacterGroupApparatusAtFamily P asserts it for every q. Primality of q sits inside the binders, so the predicates hold vacuously at non-prime q.