The bad primes of a Weierstrass curve, and the arithmetic away from them #

Let W : y² = f(x) = x³ + a₂x² + a₄x + a₆ be an elliptic curve in characteristic ≠ 2 normal form over a field K, and let R be a Dedekind domain with fraction field K. The bad primes of W over R are the primes dividing 2 or the discriminant Δ, together with those occurring in a denominator of a₂, a₄ or a₆. There are finitely many of them, and away from them the Weierstrass equation is as well behaved as it can be: the coefficients are integral, the root θ of f in a field factor K[X] ⧸ (p) of the étale algebra is integral, and — this is the point of putting Δ in the set — the derivative f' θ = 3θ² + 2a₂θ + a₄ is a unit.

That last statement is the arithmetic heart of Step 6 of the weak Mordell–Weil theorem. It is proved by evaluating at θ the Bézout identity behind separable_f, which exhibits Δ as f' θ times an explicit quadratic in θ. Both factors are integral at a good prime and their product is a unit, so both are units.

Everything here is stated at a prime w of the ring of integers of a field factor that does not lie above a bad prime of R. The estimates combine into even_valuationOfNeZero_sub_root: at such a prime the valuation of x - θ is even, for (x, y) any point of W with f x ≠ 0. That is the arithmetic content of Step 6 of the weak Mordell–Weil theorem with all the group theory stripped away; TauCeti.AlgebraicGeometry.EllipticCurve.MordellWeil.SelmerGroupA puts the group theory back and reads it as membership in a Selmer group.

Main definitions #

WeierstrassCurve.Affine.badPrimes: the set S of bad primes of W over R.
WeierstrassCurve.Affine.ringOfIntegersFactor: the integral closure of R in the field factor K[X] ⧸ (p), a Dedekind domain with fraction field K[X] ⧸ (p).

Main results #

WeierstrassCurve.Affine.finite_badPrimes: there are only finitely many bad primes.
WeierstrassCurve.Affine.valuation_root_le_one: at a prime not above a bad prime, the root θ is integral.
WeierstrassCurve.Affine.valuation_deriv_root_eq_one: at a prime not above a bad prime, f' θ is a unit. This is where Δ earns its place in badPrimes.
WeierstrassCurve.Affine.valuation_cofactor_eq_one: at such a prime, if x is integral and x - θ is not a unit, then the cofactor of x - θ in the Weierstrass equation is a unit.
WeierstrassCurve.Affine.valuation_projFactor_torsion_eq_one: at such a prime, the component of the corrected 2-torsion representative x - T + fCofactor x is a unit.
WeierstrassCurve.Affine.even_valuationOfNeZero_sub_root: at such a prime, the valuation of x - θ is even. This is the arithmetic core of Step 6.

Implementation notes #

The Valuation lemmas about the monic cubic t³ + at² + bt + c used to live here as private plumbing, on the grounds that this file and its sequel were their only consumers. The two public statements now sit with the general statements they specialize, in TauCeti.RingTheory.Valuation.RootMonic, and are used from here as Valuation dot notation; one of them, map_cubic_eq_of_one_lt, has since gained a consumer outside MordellWeil/. The coefficient helper they share stays private there. The Core section still lives in this file rather than in SelmerGroupA because it is the last consumer of the RingOfIntegers estimates above.

Roadmap #

TauCetiRoadmap/EllipticCurves/README.md, Layer 6 (Mordell–Weil), Step 6 of the weak Mordell–Weil theorem: the image of the descent map lies in A(S,2), where S is the set of bad primes defined here.

Provenance #

Adapted, with the author's proofs, from Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, pinned by TauCetiRoadmap/EllipticCurves/README.md at 66889eada51a), EllipticCurves/WeakMordellWeil.lean, sections BadPrimes, RingOfIntegers and Core (the source's Cubic section is now in TauCeti.RingTheory.Valuation.RootMonic). The source carries its own HeightOneSpectrum.below; at our Mathlib pin that map is HeightOneSpectrum.under, which is used here instead. The source is written against Lean v4.32.0; this is a forward port.