The x-coordinate of an isogeny is a rational function of x #
An isogeny φ : W₁ → W₂ commutes with negation, and negation fixes the affine coordinate x of
W₂. So the pulled-back coordinate x ∘ φ is a function on W₁ fixed by negation. The functions
fixed by negation are exactly the rational functions of x, because F(W₁) is a quadratic
extension of F(x) on which negation acts nontrivially. Hence x ∘ φ = r(x) for a unique rational
function r, written φ.xRatFunc.
Its degree, the larger of the degrees of its numerator and denominator in lowest terms, is the
degree of φ. Indeed F(W₁) and the pulled-back copy of F(W₂) both have degree two over the
copies of F(x) and F(r) they contain, and [F(x) : F(r)] is the degree of r
(RatFunc.finrank_eq_max_natDegree).
At a point the rational function computes the action of φ: φ sends an affine point (x₀, y₀)
to the point at infinity exactly when the denominator of r vanishes at x₀, and otherwise to a
point with x-coordinate r(x₀). This is what makes φ a morphism of degree deg φ on the
x-line, the input to the comparison of heights along φ.
Main definitions #
TauCeti.Isogeny.xRatFunc: the rational functionrwithx ∘ φ = r(x).
Main results #
TauCeti.Isogeny.fieldPullback_negIsogeny_eq_self_iff: a function is fixed by negation exactly when it is a rational function ofx.TauCeti.Isogeny.negIsogeny_comp: an isogeny commutes with negation.TauCeti.Isogeny.algebraMap_xRatFunc:x ∘ φ = r(x), witheq_xRatFunc_ifffor uniqueness, andfieldPullback_genericX_eq_aeval_divits formx ∘ φ = N(x) / D(x)forr = N / D.TauCeti.Isogeny.degree_eq_max_natDegree_xRatFunc:deg φis the degree ofr.TauCeti.Isogeny.natDegree_denom_lt_natDegree_num_xRatFunc: the numerator ofrhas larger degree than its denominator, asx ∘ φhas a pole at infinity.TauCeti.Isogeny.degree_eq_natDegree_num_xRatFunc: hencedeg φis the degree of the numerator ofr.TauCeti.Isogeny.pointMap_ofIsogeny_some_eq_zero_iff:φsends(x₀, y₀)to the point at infinity exactly when the denominator ofrvanishes atx₀.TauCeti.Isogeny.xCoord_pointMap_ofIsogeny_some: otherwise the image hasx-coordinater(x₀).
References #
- J. Silverman, The Arithmetic of Elliptic Curves, III.4 (isogenies) and the
proof of III.6.2(d), which computes
deg [m]as the degree ofx ∘ [m]in the same way.
The functions fixed by negation are the rational functions of x. Negation fixes x,
hence all of F(x), and does not fix y, so its fixed field lies strictly between F(x) and
F(W), which has degree two over F(x).
An isogeny commutes with negation: [-1] ∘ φ = φ ∘ [-1]. Both sides are -φ among the
morphisms, composition being additive in each variable.
The pulled-back x-coordinate is a rational function of x: it is fixed by negation.
The x-coordinate of an isogeny, as a rational function of x: the rational function r
with x ∘ φ = r(x) (algebraMap_xRatFunc), unique by eq_xRatFunc_iff.
Instances For
x ∘ φ = r(x) for the rational function r = φ.xRatFunc.
φ.xRatFunc is the only rational function r with x ∘ φ = r(x).
x ∘ φ = N(x) / D(x), for N / D = φ.xRatFunc in lowest terms.
The degree of an isogeny is the degree of its x-coordinate, the larger of the degrees of
the numerator and denominator of φ.xRatFunc in lowest terms (Silverman, proof of III.6.2(d)).
The numerator of the x-coordinate of an isogeny has larger degree than its denominator:
x ∘ φ has a pole at the point at infinity of W₁, since φ maps it to the point at infinity of
W₂, and a rational function r of x has a pole there exactly when its degree is positive.
The degree of an isogeny is the degree of the numerator of its x-coordinate, since the
numerator of φ.xRatFunc has larger degree than its denominator.
The action on points #
φ sends (x₀, y₀) to the point at infinity exactly when the denominator of its
x-coordinate vanishes at x₀.
Away from the poles, the image of (x₀, y₀) under φ has x-coordinate r(x₀), for
r = φ.xRatFunc.