Definitions/Def_ModularCurve_MazurStepThree.lean

This module introduces a single Prop-valued definition, MazurStepThree p, indexed by a natural number p; nothing is proved here. Unfolded, MazurStepThree p asserts: suppose p is prime and p \notin \{2,3,5,7,13\}; let W be a Weierstrass curve over \mathbb Z with \Delta \neq 0 satisfying the semistability condition that no prime q dividing \Delta divides c_4; let Q be a point of W base-changed along \mathbb Z \to \mathbb Q and then to \overline{\mathbb Q} (the algebraic closure AlgebraicClosure ℚ), fixed by every \mathbb Q-algebra automorphism of \overline{\mathbb Q} and of exact additive order p. Assume further that 2 \mid \Delta and Q fails W.InZeroComponentAt A for every valuation subring A \subseteq \overline{\mathbb Q} with 2 a nonunit of A, and likewise that 3 \mid \Delta with Q off the zero component at every valuation subring over 3. The conclusion is that for every prime \ell \notin \{2,3,p\} dividing \Delta and every valuation subring A of \overline{\mathbb Q} with \ell a nonunit (the predicate ValuationSubring.LiesOverPrime), Q again fails W.InZeroComponentAt A.

Here W.InZeroComponentAt A P holds when P = 0, or P = (x,y) with either x \notin A, or x, y \in A and the images of x,y in the residue field of A give a nonsingular point of W reduced to that residue field. Thus membership in the "zero component" is a condition on the chosen integral model W and on the valuation subring, expressed by reduction into the smooth locus, not via a Néron model. The behaviour of Q at 2 and at 3 is assumed rather than derived, so the statement is counting-free at those primes.