The rational place of an affine point of y² = f(x)

Let F = k(x, y) with y² = f(x) for a squarefree polynomial f ∈ k[x] of positive degree, away from characteristic two. An affine point (a, b) of the curve off the branch locus, that is with b ≠ 0, gives a place of F: there is a place P lying over the place x = a of k(x) at which y - b vanishes, and it is rational and unramified over k(x). The point (a, -b) gives the other place over x = a, the image of P under the involution y ↦ -y.

This turns concrete points of a hyperelliptic curve into places of its function field, for instance to read off the Weierstrass gaps at its unramified rational places.

Main results

• TauCeti.Place.exists_ord_sub_pos_of_sq_eq: an affine point (a, b) with b ≠ 0 is the center of a rational place of F unramified over k(x).

References

• H. Stichtenoth, Algebraic Function Fields and Codes, 2nd ed., GTM 254, Springer, 2009, Proposition 3.7.3 and Section VI.2.

theorem TauCeti.Place.exists_ord_sub_pos_of_sq_eq {k : Type u_1} {F : Type u_2} [Field k] [Field F] [Algebra (RatFunc k) F] [Algebra k F] [IsScalarTower k (RatFunc k) F] (h2 : 2 ≠ 0) {f : Polynomial k} (hf : Squarefree f) (hdeg : 0 < f.natDegree) {y : F} (hgen : (RatFunc k)⟮y⟯ = ⊤) (hy : y ^ 2 = (algebraMap (RatFunc k) F) ((algebraMap (Polynomial k) (RatFunc k)) f)) {a b : k} (hb : b ≠ 0) (hab : b ^ 2 = Polynomial.eval a f) : ∃ (P : Place k F), restrict k (RatFunc k) P = adicOfIrreducible ⋯ ∧ P.degree = 1 ∧ ramificationIdx (RatFunc k) P = 1 ∧ 0 < P.ord ((algebraMap (RatFunc k) F) RatFunc.X - (algebraMap k F) a) ∧ 0 < P.ord (y - (algebraMap k F) b)

The rational place of an affine point of y² = f(x) off the branch locus: away from characteristic two, if F = k(x, y) with y² = f(x) for a squarefree f of positive degree, and (a, b) is a point of the curve with b ≠ 0, then some place P of F over the place x = a of k(x) is rational, unramified over k(x), and has both x - a and y - b vanishing at it.