Integral points of an integral Weierstrass equation

An integral point is an affine rational point whose two coordinates come from ℤ. The equation is kept over ℤ, so negation preserves integral points even when the model is not short. A finite search over a box of integer coordinates gives a certificate for every point in that box. No finiteness assertion is made for the set of all integral points.

The set depends on the integral equation, rather than only on its rational isomorphism class. A change of variables C over ℤ, so with u = ±1 and r, s, t ∈ ℤ, identifies the rational points of C • W and of W by (x, y) ↦ (u²x + r, u³y + u²sx + t) (WeierstrassCurve.pointEquivVariableChange with L = ℚ), and this identification restricts to a bijection between their integral points (WeierstrassCurve.bijOn_pointEquivVariableChange_integralPoints). The restriction to changes of variables over ℤ matters: the scaling (x, y) ↦ (u²x, u³y) with |u| > 1 identifies the rational points too, but not the integral ones, since a point (X, Y) of W corresponds to (X / u², Y / u³).

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.1 and III.2.

def WeierstrassCurve.pointOfIntegralSolution (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (x y : ℤ) (h : W.toAffine.Equation x y) : (W.baseChange ℚ).toAffine.Point

An integral solution of the affine Weierstrass equation determines a rational point.

Equations

• W.pointOfIntegralSolution x y h = WeierstrassCurve.Affine.Point.mk ⋯

@[simp]

theorem WeierstrassCurve.pointEquiv_pointOfIntegralSolution (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (x y : ℤ) (h : W.toAffine.Equation x y) : (W.baseChange ℚ).toAffine.pointEquiv (W.pointOfIntegralSolution x y h) = some ⟨(↑x, ↑y), ⋯⟩

The affine coordinates of the rational point constructed from an integral solution.

def WeierstrassCurve.integralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] : Set (W.baseChange ℚ).toAffine.Point

The affine rational points with both coordinates integral. The point at infinity is excluded.

Equations

• W.integralPoints = {P : (W.baseChange ℚ).toAffine.Point | ∃ (x : ℤ) (y : ℤ) (h : W.toAffine.Equation x y), P = W.pointOfIntegralSolution x y h}

theorem WeierstrassCurve.mem_integralPoints_iff (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (P : (W.baseChange ℚ).toAffine.Point) : P ∈ W.integralPoints ↔ ∃ (x : ℤ) (y : ℤ) (h : W.toAffine.Equation x y), P = W.pointOfIntegralSolution x y h

A rational affine point is integral exactly when it comes from an integer solution of the Weierstrass equation.

@[simp]

theorem WeierstrassCurve.pointOfIntegralSolution_mem (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (x y : ℤ) (h : W.toAffine.Equation x y) : W.pointOfIntegralSolution x y h ∈ W.integralPoints

Every integral solution gives an integral point.

@[simp]

theorem WeierstrassCurve.zero_not_mem_integralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] : 0 ∉ W.integralPoints

The point at infinity, denoted by 0, is not an affine integral point.

theorem WeierstrassCurve.neg_mem_integralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] {P : (W.baseChange ℚ).toAffine.Point} (hP : P ∈ W.integralPoints) : -P ∈ W.integralPoints

Integral points are stable under the group inverse because -(x,y) = (x,-y-a₁x-a₃) has integral coordinates.

@[simp]

theorem WeierstrassCurve.neg_mem_integralPoints_iff (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] {P : (W.baseChange ℚ).toAffine.Point} : -P ∈ W.integralPoints ↔ P ∈ W.integralPoints

Negation preserves and reflects integrality of affine points.

def WeierstrassCurve.integralYCoordBound (W : WeierstrassCurve ℤ) (x : ℤ) : ℕ

A bound for the yCoord of an integral point with a fixed xCoord.

Equations

• W.integralYCoordBound x = (|W.a₁ * x + W.a₃| + |x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆| + 1).toNat

theorem WeierstrassCurve.abs_yCoord_le_integralYCoordBound (W : WeierstrassCurve ℤ) {x y : ℤ} (h : W.toAffine.Equation x y) : |y| ≤ ↑(W.integralYCoordBound x)

The quadratic Weierstrass equation bounds the absolute yCoord by its linear and constant coefficients. This makes a search bounded only in xCoord finite.

def WeierstrassCurve.boundedIntegralSolutions (W : WeierstrassCurve ℤ) (B : ℕ) : Finset (ℤ × ℤ)

Integer coordinate pairs with |x| ≤ B that solve the Weierstrass equation. This is a computable finite search: the ordinate bound makes each inner interval finite.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.mem_boundedIntegralSolutions_iff (W : WeierstrassCurve ℤ) (B : ℕ) (p : ℤ × ℤ) : p ∈ W.boundedIntegralSolutions B ↔ W.toAffine.Equation p.1 p.2 ∧ -↑B ≤ p.1 ∧ p.1 ≤ ↑B

The search contains exactly the integral solutions with bounded abscissa.

def WeierstrassCurve.boundedIntegralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (B : ℕ) : Finset (W.baseChange ℚ).toAffine.Point

The finite set of rational integral points with |x| ≤ B, obtained by evaluating the bounded integer-coordinate search.

Equations

• W.boundedIntegralPoints B = Finset.image (fun (p : ↥(W.boundedIntegralSolutions B)) => W.pointOfIntegralSolution (↑p).1 (↑p).2 ⋯) (W.boundedIntegralSolutions B).attach

@[simp]

theorem WeierstrassCurve.mem_boundedIntegralPoints_iff (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (B : ℕ) (P : (W.baseChange ℚ).toAffine.Point) : P ∈ W.boundedIntegralPoints B ↔ ∃ (x : ℤ) (y : ℤ) (h : W.toAffine.Equation x y), P = W.pointOfIntegralSolution x y h ∧ -↑B ≤ x ∧ x ≤ ↑B

Membership in the finite search result is exactly integrality and the abscissa bound.

theorem WeierstrassCurve.boundedIntegralPoints_subset_integralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (B : ℕ) : ↑(W.boundedIntegralPoints B) ⊆ W.integralPoints

Every point returned by the bounded search is integral.

theorem WeierstrassCurve.mem_integralPoints_iff_exists_mem_boundedIntegralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (P : (W.baseChange ℚ).toAffine.Point) : P ∈ W.integralPoints ↔ ∃ (B : ℕ), P ∈ W.boundedIntegralPoints B

The bounded searches exhaust the integral points. A claimed complete list below an abscissa bound can therefore be checked by comparing it with boundedIntegralPoints.

Changes of variables over ℤ

@[simp]

theorem WeierstrassCurve.pointEquivVariableChange_pointOfIntegralSolution (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (C : VariableChange ℤ) (x y : ℤ) (h : (C • W).toAffine.Equation x y) : (W.pointEquivVariableChange ℚ C) ((C • W).pointOfIntegralSolution x y h) = W.pointOfIntegralSolution (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) ⋯

The identification pointEquivVariableChange sends the rational point of an integral solution (x, y) of C • W to that of the integral solution (u²x + r, u³y + u²sx + t) of W.

@[simp]

theorem WeierstrassCurve.pointEquivVariableChange_symm_pointOfIntegralSolution (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (C : VariableChange ℤ) (x y : ℤ) (h : W.toAffine.Equation x y) : (W.pointEquivVariableChange ℚ C).symm (W.pointOfIntegralSolution x y h) = (C • W).pointOfIntegralSolution (↑C⁻¹.u ^ 2 * x + C⁻¹.r) (↑C⁻¹.u ^ 3 * y + ↑C⁻¹.u ^ 2 * C⁻¹.s * x + C⁻¹.t) ⋯

The inverse of pointEquivVariableChange sends the rational point of an integral solution (x, y) of W to that of the integral solution of C • W given by the coordinates of C⁻¹.

@[simp]

theorem WeierstrassCurve.pointEquivVariableChange_mem_integralPoints_iff (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (C : VariableChange ℤ) (P : ((C • W).baseChange ℚ).toAffine.Point) : (W.pointEquivVariableChange ℚ C) P ∈ W.integralPoints ↔ P ∈ (C • W).integralPoints

A change of variables over ℤ preserves and reflects integrality: a rational point of C • W is integral exactly when its image under pointEquivVariableChange is an integral point of W.

theorem WeierstrassCurve.bijOn_pointEquivVariableChange_integralPoints (W : WeierstrassCurve ℤ) [(W.baseChange ℚ).IsElliptic] (C : VariableChange ℤ) : Set.BijOn (⇑(W.pointEquivVariableChange ℚ C)) (C • W).integralPoints W.integralPoints

A change of variables over ℤ is a bijection on integral points: the identification pointEquivVariableChange of the rational points of C • W and of W maps the integral points of C • W bijectively onto those of W.