Definitions/Def_ModularCurve_StepThreeDoorPredicates.lean

Fix a natural number p with [NeZero p] (primality is never used in the bodies), an additive commutative group T, and an additive homomorphism sp : JZero p \to T out of the project's degree-zero divisor class group of the level-p modular function field; T and sp are arbitrary, standing for the Picard group of a special fibre and a specialisation map. The module only defines predicates (and one subgroup); it proves nothing. TorsBijFor ℓ sp says: for every prime q \neq \ell and every y \in T killed by some power q^n, there is an x \in JZero p killed by some power of q with sp\,x = y — i.e. surjectivity of sp on prime-to-\ell torsion only. FTorsionFor T says T is a torsion group: every y is killed by some m > 0 (it does not mention sp). CuspRuleStrongFor A sp, for a valuation subring A \subseteq \overline{\mathbb{Q}}, quantifies over a place x of the geometric function field and j_1, j_2 \in \overline{\mathbb{Q}}, together with the two hypotheses that the divisors placeDiff p x (cuspInftyBar p) and placeDiff p x (cuspZeroBar p) have degree zero, the hypothesis that x is fixed by the project's arithmetic Galois action of every \sigma \in \mathrm{Gal}(\overline{\mathbb{Q}}/\mathbb{Q}), positivity of the orders of x at jBar p - j_1 and jpBar p - j_2, and 1 < A-valuation of j_1; its conclusion is the conjunction: if v(j_2) = v(j_1)^p then sp of the class of x - \bar\infty vanishes, and if v(j_2)^p = v(j_1) then sp of the class of x - \bar 0 vanishes. In the section assuming a HeckeAlg-module structure on JZero p, spKernelImage sp is the image under sp of the Eisenstein-kernel submodule of ModularCurve_HeckeModule, RaynaudFor ℓ sp says that if \ell \neq 2 then any \ell-power-torsion element z of the rational part of the Eisenstein quotient all of whose lifts are sent by sp into spKernelImage sp must vanish, and CuspRuleFor A sp repeats CuspRuleStrongFor with both conclusions weakened from 0 to membership in spKernelImage sp.