Definitions/Def_ModularCurve_JZeroNeronAtPDataOrdCore.lean

Fix N\ge 1, a prime q with q\nmid N, and a valuation subring A of \overline{\mathbb Q} lying over q (i.e. q is a non-unit of A); let I_\lambda = A.inertiaSubgroupIn ℚ be the associated inertia subgroup of \mathrm{Gal}(\overline{\mathbb Q}/\mathbb Q) and write J = JZero (N * q) for the group of points of the modular Jacobian at level Nq. The structure JZeroNeronAtPDataOrdCore extends JZeroNeronAtPDataSameIdeal, hence carries all the data of an at-q Néron datum: three subgroup filtrations m \mapsto toric m \le fin m \le finPart m of the m-torsion J[m], each compatible with divisibility by intersection with J[m], stable under the Hecke algebra HeckeAlg = \mathbb Z[T_\ell : \ell] and under the decomposition subgroup, with finPart containing (and, for m coprime to q, equal to) the inertia-invariant m-torsion, the cyclotomic action of inertia on toric m, the inclusion \sigma x - x \in toric m for m coprime to q, the homomorphisms abq onto the m-torsion of J_0(N)^2 with kernel toric m, the finite Hecke-module \Phi of components with its specialisation maps, Eisenstein-type and Frobenius identities, a Raynaud prolongation clause, the rank formulae \#toric m= m^{r} and \#fin m=m^{r+2a}, and the two clauses detecting torsion at level N from \mathfrak m-torsion in fin q outside the toric part.

The single new field inertia_sub_mem_fin asserts Grothendieck's monodromy inclusion at every nonzero level: for all m \neq 0, all \sigma \in I_\lambda and all x \in J[m] one has \sigma\cdot x - x \in fin m. This is weaker than the inherited clause for m coprime to q, where the difference lands in toric m, but it holds for m divisible by q as well. The predicate HasJZeroNeronAtPDataOrdCore N q hqN asserts that such a datum exists for every valuation subring of \overline{\mathbb Q} lying over q.