Places of points under change of the coefficient field

Let W be an elliptic curve over a field F and f : F →+* K a homomorphism of fields. A point P of W is carried to the point f P of W.map f, and the function field F(W) embeds into K(W.map f) (WeierstrassCurve.Affine.FunctionField.map). This file compares the places of the two function fields at the points.

The place of f P restricts to the place of P, with ramification index one: the order at f P of the image of a function is its order at P. At an affine point P = (x₀, y₀) the restriction is centred at the ideal (x - x₀, y - y₀), which identifies it with the place of P up to equivalence. The ramification index is read off from a uniformizer at f P that is defined over F: one of x - f x₀ and y - f y₀ has order one, since they generate the ideal of f P. At the point at infinity the function x / y has order one on both sides.

Conversely, a place of K(W.map f) whose restriction to F(W) is equivalent to the place of P is the place of f P, and a place at which some function of F(W) has a zero or a pole restricts to a place of F(W). So the divisor of a function whose zeros and poles lie at rational points is carried to the corresponding divisor over K:

div (f^* g) = ∑ D(P) (f P)   when   div g = ∑ D(P) (P).

No hypothesis on the extension K / F is needed: it may be transcendental or inseparable.

Main results

• WeierstrassCurve.Affine.FunctionField.comap_valuation_pointEquivDegreeOnePlace_map: the place of f P restricts to the place of P.
• WeierstrassCurve.Affine.FunctionField.ord_pointEquivDegreeOnePlace_map: the order at f P of the image of a function is its order at P.
• WeierstrassCurve.Affine.FunctionField.exists_isEquiv_comap_valuation_map: a place at which the image of a function has a zero or a pole restricts to a place of F(W).
• WeierstrassCurve.Affine.FunctionField.eq_pointEquivDegreeOnePlace_mapAlong_of_isEquiv: a place restricting to the place of P is the place of f P.
• WeierstrassCurve.Affine.FunctionField.principal_map_eq_pushforward: a principal divisor supported on rational points is carried to the corresponding divisor over K.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.1–II.3.
• H. Stichtenoth, Algebraic Function Fields and Codes, III.1, III.6.

theorem WeierstrassCurve.Affine.FunctionField.isTrivialOn_comap_valuation_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) (w : TauCeti.Place K (W.map f).FunctionField) : Valuation.IsTrivialOn F (Valuation.comap (map W f) w.valuation)

The restriction of a place of K(W.map f) to F(W) is trivial on F, since f carries the constants of F(W) to constants of K(W.map f).

theorem WeierstrassCurve.Affine.FunctionField.comap_valuation_pointEquivDegreeOnePlace_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) [WeierstrassCurve.IsElliptic W] (P : W.Point) : Valuation.comap (map W f) (↑((W.map f).pointEquivDegreeOnePlace (Point.mapAlong f ⋯ P))).valuation = (↑(W.pointEquivDegreeOnePlace P)).valuation

The place of f P restricts to the place of P: for every function z on W, the value of f^* z at f P is the value of z at P.

@[simp]

theorem WeierstrassCurve.Affine.FunctionField.ord_pointEquivDegreeOnePlace_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) [WeierstrassCurve.IsElliptic W] (P : W.Point) (z : W.FunctionField) : (↑((W.map f).pointEquivDegreeOnePlace (Point.mapAlong f ⋯ P))).ord ((map W f) z) = (↑(W.pointEquivDegreeOnePlace P)).ord z

The order at f P of f^* z is the order at P of z: changing the coefficient field does not ramify the places of points.

theorem WeierstrassCurve.Affine.FunctionField.exists_isEquiv_comap_valuation_map {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) [WeierstrassCurve.IsElliptic W] (w : TauCeti.Place K (W.map f).FunctionField) {z : W.FunctionField} (hz : z ≠ 0) (hwz : w.valuation ((map W f) z) ≠ 1) : ∃ (P : TauCeti.Place F W.FunctionField), (Valuation.comap (map W f) w.valuation).IsEquiv P.valuation

A place at which the image of a function has a zero or a pole restricts to a place: if f^* z is not a unit at the place w of K(W.map f) for some z ≠ 0, then the restriction of w to F(W) is equivalent to a place of F(W).

theorem WeierstrassCurve.Affine.FunctionField.eq_pointEquivDegreeOnePlace_mapAlong_of_isEquiv {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) [WeierstrassCurve.IsElliptic W] (w : TauCeti.Place K (W.map f).FunctionField) (P : W.Point) (h : (Valuation.comap (map W f) w.valuation).IsEquiv (↑(W.pointEquivDegreeOnePlace P)).valuation) : w = ↑((W.map f).pointEquivDegreeOnePlace (Point.mapAlong f ⋯ P))

A place restricting to the place of P is the place of f P: if the restriction of a place w of K(W.map f) to F(W) is equivalent to the place of a point P of W, then w is the place of f P.

theorem WeierstrassCurve.Affine.FunctionField.principal_map_eq_pushforward {F : Type u_1} {K : Type u_2} [Field F] [Field K] (W : Affine F) (f : F →+* K) [WeierstrassCurve.IsElliptic W] {g : W.FunctionFieldˣ} {D : TauCeti.AlgebraicGeometry.WeilDivisor W.Point} (hg : TauCeti.Divisor.principal ⋯ g = (TauCeti.AlgebraicGeometry.WeilDivisor.pushforward fun (P : W.Point) => ↑(W.pointEquivDegreeOnePlace P)) D) : TauCeti.Divisor.principal ⋯ ((Units.map ↑(map W f)) g) = (TauCeti.AlgebraicGeometry.WeilDivisor.pushforward fun (P : W.Point) => ↑((W.map f).pointEquivDegreeOnePlace (Point.mapAlong f ⋯ P))) D

The divisor of a function supported on rational points, after changing the coefficient field. If the divisor of g is ∑ D(P) (P) for a divisor D on the points of W, then the divisor of f^* g is ∑ D(P) (f P).