Integrality of points on a Weierstrass curve over a unique factorization domain

Let R be a unique factorization domain with fraction field K and let W : WeierstrassCurve R have coefficients in R. This file gives the three integrality steps of the Nagell–Lutz argument that do not mention torsion.

The first is the rational-root step. If the x-coordinate of a K-point is a root of some f ∈ R[X], the rational root theorem bounds its denominator: den x ∣ f.leadingCoeff. On its own that is far from integrality — but the denominator of a point is powerful (sq_dvd_den_of_prime_of_dvd), so any prime dividing it divides it twice, hence divides f.leadingCoeff twice. If that leading coefficient is squarefree, no prime can divide the denominator at all, so den x is a unit and x is integral.

The second is a consequence of the curve equation alone: once x comes from R, y is a root of the monic quadratic Y² + (a₁x + a₃)Y − (x³ + a₂x² + a₄x + a₆) over R, so y is integral over R. That step needs no domain, fraction-field or factorisation hypothesis, so it is stated over an arbitrary R-algebra, with the IsLocalization.IsInteger form as a corollary over any commutative R-algebra in which R is integrally closed.

The third is the scaling that replaces integrality in the order-two case, the one case of Nagell–Lutz where the conclusion is weaker. Where the Y-derivative of the Weierstrass polynomial vanishes — 2y + a₁x + a₃ = 0, which is what the division-polynomial API calls ψ₂ = 0 — a bound 4x ∈ R scales to 8y ∈ R. Like the second step this needs no domain, fraction field or factorisation, only an R-algebra.

Main results

• WeierstrassCurve.isInteger_x_of_equation_of_is_root_of_squarefree_leadingCoeff: the x-coordinate of a point is integral if it is a root of a polynomial over R with squarefree leading coefficient.
• WeierstrassCurve.isIntegral_y_of_equation_of_isIntegral_x: over any R-algebra, a point whose x-coordinate is integral over R has y-coordinate integral over R.
• WeierstrassCurve.isInteger_y_of_equation_of_isInteger_x: its IsLocalization.IsInteger corollary over any commutative R-algebra in which R is integrally closed, the shape the Nagell–Lutz argument consumes.
• WeierstrassCurve.isInteger_eight_mul_y_of_evalEval_polynomialY_eq_zero: the third step, for the order-two case, where the first two do not give integrality of y. It is in the root WeierstrassCurve namespace, where W.isInteger_eight_mul_y_… elaborates; the declarations above predate that convention and scripts/lint-dot-notation.py carries them as grandfathered entries.

All three are stated for an arbitrary point: no torsion, ellipticity or minimality hypothesis. In the Nagell–Lutz argument the polynomial f is a division polynomial, whose leading coefficient is the order of the torsion point, and ψ₂ vanishes exactly at the points of order two.

This advances the Nagell–Lutz integrality milestone of TauCetiRoadmap/EllipticCurves/README.md, Layer 6, item "The torsion subgroup and Nagell–Lutz".

Provenance

Ported from the AINTLIB NagellLutz project (github.com/CBirkbeck/AINTLIB, Apache-2.0), pinned by that roadmap at dev/modular-curves @ 9fec8eba7652: LutzNagell/LutzNagellTheorem/PIDPrimeOrder.lean, declarations isInteger_of_root_squarefree_leading_coeff and y_isInteger_of_x_isInteger_on_curve. The latter is generalised here from the fraction field to an arbitrary R-algebra.

isInteger_eight_mul_y_of_evalEval_polynomialY_eq_zero is the y half of bounded_den_of_order_two_general (LutzNagell/LutzNagellTheorem/GeneralPrimeOrder.lean:176 at main @ 1c1c74664e40071c2c2165bc55ca2616a67ccd6b), which states both halves together over ℚ/ℤ as (∃ n : ℤ, (n : ℚ) = 4 * x) ∧ ∃ m : ℤ, (m : ℚ) = 8 * y for a point of order two. Two departures: the conclusion is IsLocalization.IsInteger over general R/K, so the source's isInteger_int_iff bridge is not needed; and the two-torsion hypothesis is weakened to the vanishing of polynomialY, which is what the y half actually uses and which makes the statement independent of the point-level [n]-multiplication development. The x half is separately the merged den_dvd_four_of_order_two.

theorem WeierstrassCurve.isIntegral_y_of_equation_of_isIntegral_x {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {A : Type u_2} [CommRing A] [Algebra R A] {x y : A} (h : (W.baseChange A).toAffine.Equation x y) (hx : IsIntegral R x) : IsIntegral R y

An integral x-coordinate forces an integral y-coordinate, over any R-algebra.

On the curve, y is a root of the monic quadratic Y² + (a₁x + a₃)Y − (x³ + a₂x² + a₄x + a₆), whose coefficients are polynomial in x and so are integral whenever x is. No domain, fraction-field or factorisation hypothesis is needed, and x need not come from R itself.

theorem WeierstrassCurve.isInteger_x_of_equation_of_is_root_of_squarefree_leadingCoeff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] {x y : K} [IsDomain R] [UniqueFactorizationMonoid R] (h : (W.baseChange K).toAffine.Equation x y) {f : Polynomial R} (hroot : (Polynomial.aeval x) f = 0) (hsf : Squarefree f.leadingCoeff) : IsLocalization.IsInteger R x

The rational-root integrality step. If the x-coordinate of a point of W is a root of f ∈ R[X] and f.leadingCoeff is squarefree, then x is integral.

The rational root theorem gives den x ∣ f.leadingCoeff; powerfulness of the denominator (sq_dvd_den_of_prime_of_dvd) upgrades any prime factor q of den x to q * q ∣ f.leadingCoeff, which squarefreeness forbids.

theorem WeierstrassCurve.isInteger_y_of_equation_of_isInteger_x {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {K : Type u_2} [CommRing K] [Algebra R K] [IsIntegrallyClosedIn R K] {x y : K} (h : (W.baseChange K).toAffine.Equation x y) (hx : IsLocalization.IsInteger R x) : IsLocalization.IsInteger R y

On the curve, an integral x-coordinate forces an integral y-coordinate. The IsLocalization.IsInteger form of isIntegral_y_of_equation_of_isIntegral_x, which is the shape the Nagell–Lutz argument consumes.

K need not be a fraction field of R, nor even a field: integral closedness relative to K is what the argument uses, over any commutative R-algebra. It is strictly weaker than [IsIntegrallyClosed R] [IsFractionRing R K] — those two imply it (isIntegrallyClosed_iff_isIntegrallyClosedIn, and Mathlib supplies the instance), but not conversely.

theorem WeierstrassCurve.isInteger_eight_mul_y_of_evalEval_polynomialY_eq_zero {R : Type u_1} [CommRing R] {K : Type u_2} [CommRing K] [Algebra R K] (W : WeierstrassCurve R) {x y : K} (hy : Polynomial.evalEval x y (W.baseChange K).toAffine.polynomialY = 0) (hx : IsLocalization.IsInteger R (4 * x)) : IsLocalization.IsInteger R (8 * y)

Where the Y-derivative vanishes, a bound on x scales to one on y: if polynomialY vanishes at (x, y) and 4x is integral, then 8y is integral.

This is the y half of the order-two exception in Nagell–Lutz — the case where a torsion point need not have integral coordinates at all, and where 8y rather than y is what lies in R. polynomialY is ∂/∂Y of the Weierstrass polynomial, evaluating to 2y + a₁x + a₃, and is what the division-polynomial API calls ψ₂. Taking its vanishing as the hypothesis is strictly weaker than two-torsion and needs no field, no fraction ring and no Nonsingular: a point of order two satisfies it, and so does any pair at which ψ₂ happens to vanish.