Integrality descends along multiplication by n

If n • P has integral coordinates then so does P. This is the descent step of the Nagell–Lutz argument: it lets an integrality claim about a torsion point be pulled back from a multiple where it is easier to establish.

The mechanism is one identity between the two x-coordinates. zsmul_point_eq_smulEval gives the Jacobian coordinates of n • P as (φₙ : ωₙ : ψₙ) evaluated at P, and comparing that with the affine representative of n • P yields x' · ΨSqₙ(x) = Φₙ(x). Writing x' as algebraMap R K c for the c : R its integrality supplies, that exhibits x as a root of the monic polynomial Φₙ − C c · ΨSqₙ over R, so integral closure places x in R, and the curve equation carries integrality from x to y.

Main results

• WeierstrassCurve.smulEval_equiv_of_zsmul: the division-polynomial triple at P represents n • P in Jacobian coordinates; the two coordinate identities below are read off it.
• WeierstrassCurve.mul_eval_ΨSq_eq_eval_Φ_of_zsmul: the coordinate identity x' · ΨSqₙ(x) = Φₙ(x) relating P and n • P, over a field.
• WeierstrassCurve.mul_evalEval_ψ_cube_eq_evalEval_ω_of_zsmul: its y-coordinate companion y' · ψₙ(P)³ = ωₙ(P).
• WeierstrassCurve.isInteger_of_zsmul_isInteger: the descent step. Over a base R integrally closed in K, if n • P = P' and P' has integral x-coordinate, both coordinates of P are integral.

Roadmap

New mathematics: TauCetiRoadmap/EllipticCurves/README.md:821 — "The torsion subgroup and Nagell–Lutz", route "division polynomials" (:830–:831). This is the descent half of that route; it is a prerequisite of the roadmap's stated theorem rather than the theorem itself.

Provenance

Ported from J. Xu and D. K. Angdinata's projects/NagellLutz/LutzNagell/LutzNagellTheorem/PIDIntegralMultiple.lean in AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0, main @ 1c1c74664e40071c2c2165bc55ca2616a67ccd6b): x_coord_nsmul_eq (:48) and isInteger_of_nsmul_isInteger (:93). The file is byte-identical at 9fec8eba7652, the revision the roadmap pins for this project (README:1072), verified by blob hash, so the citations hold at either.

The source's intermediate x_isInteger_of_nsmul_x_isInteger (:73) is not ported: it is the composition of the coordinate identity above with the integral-root argument, and this repository already carries the latter as Integral.lean's isInteger_of_mul_eval_ΨSq_eq_eval_Φ — whose own docstring notes that "no point, and no multiple, occurs in this statement", i.e. it is exactly the point-free half. The composition is inlined here rather than given a name.

Three adaptations. curveK R K W is W.map (algebraMap R K), which is rfl-equal to Mathlib's W.baseChange K; this file uses baseChange, matching Integral.lean and Integrality.lean. The source's hn : n ≠ 0, hn_R : (n : R) ≠ 0 and _hy' hypotheses are dropped — none is used by the proof once the integral-root step is delegated, and _hy' is unused upstream too.

The base ring is generalised, and K need not be its fraction field. The source assumes a UFD; no factorisation argument occurs anywhere in these two proofs, so integral closedness alone suffices, and [IsDomain R] turns out to be unnecessary as well — unusedSectionVars reported it once the UFD hypothesis was removed. Integral closedness is then asked for relative to K, as [IsIntegrallyClosedIn R K], rather than as [IsIntegrallyClosed R] [IsFractionRing R K]: this is the hypothesis Integral.lean's isInteger_of_mul_eval_ΨSq_eq_eval_Φ already takes, and it is strictly weaker, since the pair implies it (isIntegrallyClosed_iff_isIntegrallyClosedIn) but says more besides. The y-coordinate step is then exactly Integrality.lean's isInteger_y_of_equation_of_isInteger_x, which asks for [IsIntegrallyClosedIn R K] and nothing else — the same hypothesis this file already carries, so it applies with no bridging.

[DecidableEq K] is not removable: n • P is zsmul for Mathlib's AddCommGroup W.Point instance, which is declared under [DecidableEq F] because affine addition is defined by cases. The instance is needed to state both theorems, so a classical inside the proofs cannot supply it.

theorem WeierstrassCurve.smulEval_equiv_of_zsmul {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) {x y : F} (hns : E.toAffine.Nonsingular x y) {x' y' : F} (hns' : E.toAffine.Nonsingular x' y') {n : ℤ} (hnP : n • Affine.Point.some x y hns = Affine.Point.some x' y' hns') : E.smulEval x y n ≈ ![x', y', 1]

The division-polynomial triple at P represents n • P, so it agrees with the affine representative of that value up to a unit scalar. Both coordinate identities below are one coordinate of this single equivalence.

theorem WeierstrassCurve.mul_eval_ΨSq_eq_eval_Φ_of_zsmul {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) {x y : F} (hns : E.toAffine.Nonsingular x y) {x' y' : F} (hns' : E.toAffine.Nonsingular x' y') {n : ℤ} (hnP : n • Affine.Point.some x y hns = Affine.Point.some x' y' hns') : x' * Polynomial.eval x (E.ΨSq n) = Polynomial.eval x (E.Φ n)

The x-coordinates of P and n • P satisfy x' · ΨSqₙ(x) = Φₙ(x).

The division-polynomial formula for the x-coordinate of a multiple, cleared of its denominator, so that it holds with no side condition on ΨSqₙ(x) vanishing.

theorem WeierstrassCurve.mul_evalEval_ψ_cube_eq_evalEval_ω_of_zsmul {F : Type u_1} [Field F] [DecidableEq F] (E : WeierstrassCurve F) {x y : F} (hns : E.toAffine.Nonsingular x y) {x' y' : F} (hns' : E.toAffine.Nonsingular x' y') {n : ℤ} (hnP : n • Affine.Point.some x y hns = Affine.Point.some x' y' hns') : y' * Polynomial.evalEval x y (E.ψ n) ^ 3 = Polynomial.evalEval x y (E.ω n)

The y-coordinates of P and n • P satisfy y' · ψₙ(P)³ = ωₙ(P).

The companion of mul_eval_ΨSq_eq_eval_Φ_of_zsmul for the second coordinate, cleared of its denominator in the same way. The two identities together pin n • P down, which the x-identity alone cannot, because a point and its negative share an x-coordinate. The hypothesis n • P = (x', y') forces ψₙ(P) ≠ 0, since the two Jacobian representatives differ by a unit scalar acting on the Z-coordinate.

theorem WeierstrassCurve.isInteger_of_zsmul_isInteger {R : Type u_2} [CommRing R] {K : Type u_3} [Field K] [DecidableEq K] [Algebra R K] [IsIntegrallyClosedIn R K] (W : WeierstrassCurve R) {x y : K} (hns : (W.baseChange K).toAffine.Nonsingular x y) {n : ℤ} {x' y' : K} (hns' : (W.baseChange K).toAffine.Nonsingular x' y') (hnP : n • Affine.Point.some x y hns = Affine.Point.some x' y' hns') (hx' : IsLocalization.IsInteger R x') : IsLocalization.IsInteger R x ∧ IsLocalization.IsInteger R y

Integrality descends along multiplication by n. If n • P = P' and P' has integral x-coordinate, then both coordinates of P are integral.

The conclusion is for every n, with no primality, no bound on the order of P, and no hypothesis that P is torsion at all.