Definitions/Def_ModularCurve_JZeroGoodReductionV2.lean

Fix a valuation subring A of \overline{\mathbb{Q}}, a prime \ell (with proof hℓ), and a level N \neq 0, and assume the project's Hecke algebra HeckeAlg acts on both JZero N and on \mathrm{Pic}^0 of the function field modularFunctionFieldC (ResidueField A) N over the residue field of A. The structure JZeroGoodReductionSpecialization bundles, as data and fields, a specialisation situation in characteristic \ell: an additive group homomorphism sp from JZero N to that \mathrm{Pic}^0, an additive endomorphism F of the target (the intended geometric Frobenius), and five properties asserted as structure fields — hsurj, surjectivity of sp; hecke_comm, \mathrm{sp}(T\cdot x) = T\cdot \mathrm{sp}(x) for every T \in HeckeAlg; inertia_comm, \mathrm{sp}(\sigma\cdot x) = \mathrm{sp}(x) for every \sigma in A.inertiaSubgroupIn ℚ; frobenius_comm, \mathrm{sp}(\sigma\cdot x) = F(\mathrm{sp}(x)) for every \sigma \in \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}) satisfying A.IsFrobeniusAt σ ℓ; and injective_torsion, injectivity of sp on p-power torsion for every prime p \neq \ell (explicitly: if p^n\cdot x = 0 for some n and \mathrm{sp}(x)=0 then x=0). The primality guard on p matters: without it the case p = 0 would force sp to be injective outright. A final field sfr asserts the project's predicate SpecialFibreRelation ℓ hℓ F for this F (the intended Eichler–Shimura relation); that predicate, like IsSpecialization, JZero, Pic0, modularFunctionFieldC and heckeGen, is defined in the imported project modules. Nothing in the structure refers to a Néron model or to reduction of curves; the geometric content is carried entirely by the assumed fields.

Three small lemmas follow: hgen, that the kernel of sp is stable under each Hecke generator heckeGen q; toIsSpecialization, extracting from the bundle the project's predicate IsSpecialization p (JZero N) … A ℓ D.sp D.F for any prime p \neq \ell; and toSpecializationExistsBody, the conjunction of that predicate with SpecialFibreRelation. Two local instances supply decidable equality on the residue field (classically) and the residue-field algebra structure on the modular function field.