Definitions/Def_ModularCurve_JZeroGoodReductionV3.lean

Fix a valuation subring A of \overline{\mathbb{Q}}, a prime \ell and N \neq 0, and work with J_0(N) = JZero N, the degree-zero divisor class group of the modular function field over \overline{\mathbb{Q}}, and with J' = Pic0 (ResidueField A) (modularFunctionFieldC (ResidueField A) N), the corresponding group for the field obtained by adjoining to the residue field k = ResidueField A inside k((q)) the two Laurent series jqModC k and its N-fold q-substitute jqNModC k N; both carry HeckeAlg-module structures, HeckeAlg being the polynomial algebra \mathbb{Z}[T_q : q \text{ prime}] with generators heckeGen q. The structure JZeroGoodReductionSpecialization_alt bundles an additive map sp : J_0(N) \to J' and an additive endomorphism F of J', together with: surjectivity of sp; full HeckeAlg-equivariance sp(T\cdot x) = T\cdot sp(x); invariance sp(\sigma \cdot x) = sp(x) for \sigma in the inertia subgroup of A over \mathbb{Q}; the identity sp(\sigma \cdot x) = F(sp(x)) for every \sigma which is a Frobenius at A for \ell (i.e. lies in the decomposition subgroup and acts on k as x \mapsto x^{\ell}); injectivity of sp on p-power torsion for every natural number p with \ell \nmid p; and the field sfr, asserting the special-fibre relation F^2(y) - T_\ell F(y) + \ell y = 0 for all y \in J'.

The torsion clause here is indexed by all p not divisible by \ell (thus excluding p = 0 and multiples of \ell), rather than by primes p \neq \ell. Accompanying results record that \ker(sp) is stable under each heckeGen q, and convert the data, for any p with \ell \nmid p, into IsSpecialization for that p and into the conjunction of IsSpecialization with SpecialFibreRelation required by SpecializationExists.