Denominators 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. Writing a K-point of W as a pair of reduced fractions x = num x / den x and y = num y / den y (Mathlib's IsFractionRing.num and IsFractionRing.den), the Weierstrass equation forces the denominator of the x-coordinate to be powerful: a prime dividing it divides it at least twice. In particular den x is never a prime element — the form in which the Nagell–Lutz integrality argument uses it, where the rational root theorem has already bounded den x by a prime.

This is weaker than the classical statement for a short model y² = x³ + Ax + B over ℤ, that den x = d² and den y = d³ for some d: that needs each q-adic valuation of den x to be even, not merely at least 2. For a short model that parity follows from comparing valuations across y² = x³ + Ax + B; no such argument is carried out here, and the statement below is the weaker one the Nagell–Lutz route consumes.

The proof is a descent in three steps. Clearing denominators in the Weierstrass equation gives an identity in R; if a prime q divides den x exactly once, then dividing that identity by successive powers of q forces q ^ 2 ∣ den y and then q ∣ num y — contradicting the reducedness of y.

Main results

• WeierstrassCurve.sq_dvd_den_of_prime_of_dvd: a prime dividing the denominator of the x-coordinate of a point divides it at least twice.
• WeierstrassCurve.not_prime_den: the denominator of the x-coordinate of a point is not a prime element.
• WeierstrassCurve.isUnit_den_of_dvd_squarefree: a squarefree bound on that denominator forces it to be a unit.
• WeierstrassCurve.den_eq_one_of_dvd_squarefree: the same over ℤ, where it says the rational x-coordinate is an integer — the conclusion the rational root theorem feeds into.

This is the denominator input to the Nagell–Lutz integrality milestone of TauCetiRoadmap/EllipticCurves/README.md, Layer 6, item "The torsion subgroup and Nagell–Lutz". No torsion hypothesis is needed here: the statements hold for every point.

Provenance

Ported from the AINTLIB NagellLutz project (github.com/CBirkbeck/AINTLIB, Apache-2.0), pinned by that roadmap at dev/modular-curves @ 9fec8eba7652: the descent follows LutzNagell/LutzNagellTheorem/PIDDenominators.lean (den_no_simple_prime_factor_of_on_curve, den_not_prime_of_on_curve) and its positive restatement den_powerful_of_on_curve in LutzNagell/LutzNagellTheorem/PIDMain.lean.

The ℚ/ℤ conclusion follows LutzNagell/LutzNagellTheorem/GeneralDenominators.lean, declaration den_ne_prime_of_on_general_curve. That source states the prime-denominator exclusion — extra hypothesis x.den = p for a prime p, conclusion False — and names the divisibility consequence in its docstring without stating it; den_eq_one_of_dvd_squarefree is that consequence, with a squarefree bound in place of a prime one.

theorem WeierstrassCurve.sq_dvd_den_of_prime_of_dvd {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve R) {x y : K} {q : R} (h : (W.baseChange K).toAffine.Equation x y) (hq : Prime q) (hqd : q ∣ ↑(IsFractionRing.den R x)) : q ^ 2 ∣ ↑(IsFractionRing.den R x)

The denominator of the x-coordinate of a point is powerful.

If (x, y) is a point of W over the fraction field K of a unique factorization domain R, then a prime of R dividing the denominator of x divides it at least twice.

theorem WeierstrassCurve.isUnit_den_of_dvd_squarefree {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve R) {x y : K} (h : (W.baseChange K).toAffine.Equation x y) {m : R} (hsf : Squarefree m) (hdvd : ↑(IsFractionRing.den R x) ∣ m) : IsUnit ↑(IsFractionRing.den R x)

A squarefree bound on the denominator forces it to be a unit.

A prime dividing the denominator divides it twice (sq_dvd_den_of_prime_of_dvd), so it would divide any bound twice as well; a squarefree bound admits no such prime, leaving the denominator without prime factors.

theorem WeierstrassCurve.not_prime_den {R : Type u_1} [CommRing R] [IsDomain R] [UniqueFactorizationMonoid R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (W : WeierstrassCurve R) {x y : K} (h : (W.baseChange K).toAffine.Equation x y) : ¬Prime ↑(IsFractionRing.den R x)

The denominator of the x-coordinate of a point is not prime.

The Nagell–Lutz form of WeierstrassCurve.sq_dvd_den_of_prime_of_dvd: a prime element is not divisible by its own square, so it cannot be the denominator of the x-coordinate of a point.

theorem WeierstrassCurve.den_eq_one_of_dvd_squarefree {W : WeierstrassCurve ℤ} {x y : ℚ} (h : (W.baseChange ℚ).toAffine.Equation x y) {m : ℕ} (hsf : Squarefree m) (hdvd : x.den ∣ m) : x.den = 1

A rational point whose x-denominator divides a squarefree number has an integral x-coordinate.

The ℚ/ℤ form of isUnit_den_of_dvd_squarefree, which is what the Nagell–Lutz integrality argument consumes: the rational root theorem bounds x.den, and a squarefree bound leaves the denominator a unit, hence 1. Over ℤ the ring-theoretic denominator and the numeral agree up to sign (Rat.isFractionRingDen).