Every x-coordinate of a Weierstrass curve over an algebraically closed field is attained

Fixing x = a in the Weierstrass equation leaves a monic quadratic in y, so over an algebraically closed field it has a root and a is the x-coordinate of a solution. The statement is about Affine.Equation alone: no nonsingularity, no ellipticity, and no division polynomial is involved, which is why it lives here rather than with any consumer.

Main results

• WeierstrassCurve.Affine.exists_point_on_curve: over an algebraically closed field every element is the x-coordinate of a solution of W.Equation.
• WeierstrassCurve.mem_range_y_of_equation_of_mem_range_x: over an algebraically closed field, a solution of W.Equation whose x-coordinate lies in the image of F has its y-coordinate there too.

Stated for an arbitrary affine Weierstrass curve over an algebraically closed field. It yields a solution of the equation, not an element of W.Point; a caller wanting a point pairs it with equation_iff_nonsingular_of_Δ_ne_zero or equation_iff_nonsingular, which is what makes the hypothesis-free form the useful one.

Roadmap

TauCetiRoadmap/EllipticCurves/README.md:99 — "[n] is division polynomials". The consumer is DivisionPolynomial/Coprimality.lean, whose proof of isCoprime_Φ_ΨSq passes to the algebraic closure and needs a common root of Φₙ and ΨSqₙ to be the x-coordinate of an actual point. Nothing here mentions a division polynomial.

Provenance

Ported, with the author's proof, from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), the HasseWeil project at dev/hasse-weil @ 513e83879e2f — the revision TauCetiRoadmap/EllipticCurves/README.md:1071 pins for that project. Source file projects/HasseWeil/HasseWeil/Auxiliary/DivisionPolynomial.lean, section Coprimality, declaration exists_point_on_curve, whose header credits David Kurniadi Angdinata and Junyan Xu. Upstream it sits beside its coprimality consumer and is stated for a global WeierstrassCurve; here it is separated out and stated for the affine model, which is the level its content lives at. The degree of the quadratic is Polynomial.degree_quadratic here in place of the source's explicit natDegree bound.

theorem WeierstrassCurve.Affine.exists_point_on_curve {F : Type u_1} [Field F] [IsAlgClosed F] (W : Affine F) (a : F) : ∃ (b : F), W.Equation a b

Over an algebraically closed field every x-coordinate is realised by a point. Solving the Weierstrass equation for y at a fixed x is finding a root of a quadratic, which an algebraically closed field always has.

theorem WeierstrassCurve.mem_range_y_of_equation_of_mem_range_x {F : Type u_1} [Field F] [IsAlgClosed F] (W : WeierstrassCurve F) {Ω : Type u_2} [Field Ω] [Algebra F Ω] {x y : Ω} (heq : (W.baseChange Ω).toAffine.Equation x y) {x₀ : F} (hx : (algebraMap F Ω) x₀ = x) : y ∈ Set.range ⇑(algebraMap F Ω)

The y-coordinate of a point with rational x is rational when the base field is algebraically closed: integrality then puts it in the image of F.