Which x-coordinates of a Weierstrass curve are attained over a separably closed field

Fixing x = a in the Weierstrass equation leaves the monic quadratic Y² + (a₁a + a₃)Y − (a³ + a₂a² + a₄a + a₆) in Y, whose derivative is 2Y + (a₁a + a₃). A separably closed field has a root of it unless that derivative vanishes identically, which happens only in characteristic 2 at an a with a₁a + a₃ = 0. So a is the x-coordinate of a solution away from that case. Combined with the general coordinate descent lemma from Affine.BaseChange, this shows that a solution whose x-coordinate is already rational has a rational y-coordinate too.

The excluded case is real. Over the separable closure of 𝔽₂(t) the equation y² + y = x³ + t has a₁a + a₃ = 1, but y² = x³ + t — where a₁ = a₃ = 0 — has y = √(a³ + t), which is purely inseparable over the base field and need not lie in it. Both statements are about Affine.Equation alone: no nonsingularity and no ellipticity is involved.

The two results are the separably closed companions of exists_point_on_curve and mem_range_y_of_equation_of_mem_range_x, which need no side condition because an algebraically closed field also extracts the inseparable square root.

Main results

• WeierstrassCurve.Affine.exists_point_on_curve_of_isSepClosed: over a separably closed field, an element at which the quadratic in y is separable is the x-coordinate of a solution of W.Equation.
• WeierstrassCurve.mem_range_y_of_equation_of_mem_range_x_of_isSepClosed: such a solution over an extension, with x-coordinate in the image of the base field, has its y-coordinate there too.

theorem WeierstrassCurve.Affine.exists_point_on_curve_of_isSepClosed {F : Type u_1} [Field F] [IsSepClosed F] (W : Affine F) (a : F) (h : 2 ≠ 0 ∨ W.a₁ * a + W.a₃ ≠ 0) : ∃ (b : F), W.Equation a b

Over a separably closed field an x-coordinate is realised by a point as soon as the quadratic in y it leaves behind is separable, which is the hypothesis 2 ≠ 0 ∨ a₁a + a₃ ≠ 0. In characteristic 2 at an a with a₁a + a₃ = 0 the equation reads y² = a³ + a₂a² + a₄a + a₆, whose solution is purely inseparable over the base field and need not lie in it.

theorem WeierstrassCurve.mem_range_y_of_equation_of_mem_range_x_of_isSepClosed {F : Type u_1} [Field F] (W : WeierstrassCurve F) {Ω : Type u_2} [CommRing Ω] [NoZeroDivisors Ω] [Algebra F Ω] {x y : Ω} [IsSepClosed F] (heq : (W.baseChange Ω).toAffine.Equation x y) {x₀ : F} (hx : (algebraMap F Ω) x₀ = x) (h : 2 ≠ 0 ∨ W.a₁ * x₀ + W.a₃ ≠ 0) : y ∈ Set.range ⇑(algebraMap F Ω)

The y-coordinate of a point with rational x is rational over a separably closed field, under the same separability side condition as Affine.exists_point_on_curve_of_isSepClosed.