Points of infinite order, certified by reduction at two primes

Let A be a Dedekind domain with fraction field F, and let W be an elliptic curve over F with good reduction at a height-one prime u of A, so that reduction of points is a group homomorphism W(F) →+ W_k(k) to the points of the reduced curve. Reduction is injective on the torsion of order prime to u (Silverman AEC VII.3.1). So if a natural number ℓ ∉ u divides the order of a torsion point P, it also divides the order of the reduction of P (WeierstrassCurve.Affine.Point.dvd_addOrderOf_reductionHom).

This gives a finite certificate that a rational point has infinite order. Suppose P ≠ 0, that p ∈ u and q ∈ u' for two primes u and u' of good reduction, and that the reductions of P are killed by m and n respectively. A prime ℓ dividing the order of a torsion point P divides p * m: it divides p when ℓ ∈ u, and otherwise it divides the order of the reduction, which divides m. Likewise ℓ ∣ q * n. So when p * m and q * n are coprime, P is not torsion (WeierstrassCurve.Affine.Point.not_isOfFinAddOrder_of_coprime). For a curve over ℚ this is a computation in two finite point groups W(𝔽_p) and W(𝔽_q), and a point of infinite order shows that the Mordell–Weil rank is positive.

Only the injectivity on torsion prime to the residue characteristic is used, which is why the residue characteristics p and q enter the coprimality condition: torsion of p-power order may reduce to zero modulo u.

Main results

All results are in the namespace WeierstrassCurve.Affine.Point.

• dvd_addOrderOf_reductionHom: at good reduction, a natural number ℓ ∉ u dividing the order of a torsion point divides the order of its reduction.
• prime_dvd_mul_of_dvd_addOrderOf: if p ∈ u and the reduction of a torsion point P is killed by m, every prime dividing the order of P divides p * m.
• not_isOfFinAddOrder_of_coprime: the two-prime certificate that a point has infinite order.

Provenance

The two-prime certificate follows WeierstrassCurve.Affine.not_isOfFinAddOrder_of_coprime_red in Michael Stoll's EllipticCurves project (github.com/MichaelStollBayreuth/EllipticCurves, Apache-2.0, commit 3bfe124), EllipticCurves/InfiniteOrder.lean. That version assumes injectivity of reduction on all torsion, available when p ∉ u ^ (p - 1), and asks only that m and n be coprime. The version here uses injectivity on torsion prime to u alone, so the residue characteristics enter the coprimality condition, and it is derived from the prime-by-prime statement prime_dvd_mul_of_dvd_addOrderOf.

References

• J. Silverman, The Arithmetic of Elliptic Curves, VII.3.1 and VIII.7.

theorem WeierstrassCurve.Affine.Point.dvd_addOrderOf_reductionHom {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] [DecidableEq F] (u : IsDedekindDomain.HeightOneSpectrum A) {W : Affine F} [IsIntegral (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring) W] [(integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring) W).IsElliptic] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring)] {P : W.Point} (hP : IsOfFinAddOrder P) {ℓ : ℕ} (hℓu : ↑ℓ ∉ u.asIdeal) (hℓP : ℓ ∣ addOrderOf P) : ℓ ∣ addOrderOf ((reductionHom (IsDedekindDomain.HeightOneSpectrum.valuation F u)) P)

At good reduction, reduction keeps the divisors ℓ ∉ u of the order of a torsion point: if a natural number ℓ ∉ u divides the order of a torsion point P, it divides the order of the reduction of P.

theorem WeierstrassCurve.Affine.Point.prime_dvd_mul_of_dvd_addOrderOf {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] [DecidableEq F] (u : IsDedekindDomain.HeightOneSpectrum A) {W : Affine F} [IsIntegral (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring) W] [(integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring) W).IsElliptic] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring)] {P : W.Point} (hP : IsOfFinAddOrder P) {ℓ : ℕ} (hℓ : Nat.Prime ℓ) (hℓP : ℓ ∣ addOrderOf P) {p m : ℕ} (hp : ↑p ∈ u.asIdeal) (hm : m • (reductionHom (IsDedekindDomain.HeightOneSpectrum.valuation F u)) P = 0) : ℓ ∣ p * m

The primes of the order of a torsion point, seen at one prime of good reduction: if p ∈ u and the reduction of a torsion point P is killed by m, every prime dividing the order of P divides p * m.

theorem WeierstrassCurve.Affine.Point.not_isOfFinAddOrder_of_coprime {A : Type u_1} [CommRing A] [IsDedekindDomain A] {F : Type u_2} [Field F] [Algebra A F] [IsFractionRing A F] [DecidableEq F] (u : IsDedekindDomain.HeightOneSpectrum A) {W : Affine F} (u' : IsDedekindDomain.HeightOneSpectrum A) [IsIntegral (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring) W] [(integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring) W).IsElliptic] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.valuation F u).valuationSubring)] [IsIntegral (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u').valuationSubring) W] [(integralModel (↥(IsDedekindDomain.HeightOneSpectrum.valuation F u').valuationSubring) W).IsElliptic] [DecidableEq (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.valuation F u').valuationSubring)] {P : W.Point} (hP : P ≠ 0) {p q m n : ℕ} (hp : ↑p ∈ u.asIdeal) (hq : ↑q ∈ u'.asIdeal) (hmn : (p * m).Coprime (q * n)) (hm : m • (reductionHom (IsDedekindDomain.HeightOneSpectrum.valuation F u)) P = 0) (hn : n • (reductionHom (IsDedekindDomain.HeightOneSpectrum.valuation F u')) P = 0) : ¬IsOfFinAddOrder P

A point of infinite order, certified by reduction at two primes. Let u and u' be primes of good reduction for W, with p ∈ u and q ∈ u', and let P ≠ 0 be a point whose reductions at u and u' are killed by m and n. If p * m and q * n are coprime, P has infinite order. Over ℚ, p and q are the residue characteristics and the hypotheses on m and n are computations in the finite groups W(𝔽_p) and W(𝔽_q).