The place at infinity of F(W) over F(x)

For a Weierstrass curve W over a field F, the place at infinity of the function field F(W) lies over the place at infinity of the rational function field F(x), with ramification index 2: the order at infinity of a rational function of x is twice its order at infinity in F(x). When the coordinate ring of W is a Dedekind domain, for instance when W is an elliptic curve, it is the only place of F(W) over that place.

Main results

• TauCeti.Place.ord_infinity_algebraMap: the order at infinity of a rational function of x is twice its order at ∞.
• TauCeti.Place.restrict_infinity: the place at infinity of F(W) restricts to ∞ on F(x).
• TauCeti.Place.ramificationIdx_infinity: its ramification index over F(x) is 2.
• TauCeti.Place.restrict_eq_infty_iff: for a Dedekind coordinate ring, it is the only place of F(W) over ∞.

@[simp]

theorem TauCeti.Place.ord_infinity_algebraMap {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) (r : RatFunc F) : (infinity W).ord ((algebraMap (RatFunc F) W.FunctionField) r) = 2 * (infty F).ord r

The order at infinity of a rational function of x is twice its order at the place at infinity of F(x).

@[simp]

theorem TauCeti.Place.restrict_infinity {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : restrict F (RatFunc F) (infinity W) = infty F

The place at infinity of F(W) lies over the place at infinity of F(x).

@[simp]

theorem TauCeti.Place.ramificationIdx_infinity {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) : ramificationIdx (RatFunc F) (infinity W) = 2

The place at infinity of F(W) has ramification index 2 over F(x).

@[simp]

theorem TauCeti.Place.restrict_eq_infty_iff {F : Type u_1} [Field F] (W : WeierstrassCurve.Affine F) [IsDedekindDomain W.CoordinateRing] (Q : Place F W.FunctionField) : restrict F (RatFunc F) Q = infty F ↔ Q = infinity W

The place at infinity is the only place of F(W) over the place at infinity of F(x): every other place comes from a height-one prime of the coordinate ring, so x is regular there, while x has a pole at ∞.