The degree of the rational function Φₙ / ΨSqₙ

Coprimality.lean shows that Φₙ and ΨSqₙ are coprime on a nonsingular curve, so for n ≠ 0 the quotient Φₙ / ΨSqₙ is already in lowest terms. This file draws the consequence: it has degree n², in the sense that adjoining it to F inside F(x) leaves an extension of dimension n².

For n ≠ 0 that quotient is the x-coordinate of n • (x, y), so the theorem says the x-coordinate map of [n] is a rational map of degree n². At n = 0 it is not a coordinate of anything — [0] sends every point to infinity, and ΨSq₀ = 0 makes the quotient the junk value 0 — but the theorem still holds there, as an equality of two zeros; see its docstring.

This is the arithmetic half of deg [n] = n² (Silverman III.6.4(a), proved in III.6.2(d)). The other half is the tower F(x, y) over F(x), which is quadratic on both storeys and therefore cancels; neither that nor the isogeny [n] itself appears here.

Main results

• WeierstrassCurve.finrank_adjoin_Φ_div_ΨSq: [F(x) : F(Φₙ/ΨSqₙ)] = n².

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.4(a), whose proof is III.6.2(d).

Provenance

Adapted from the AINTLIB HasseWeil project (github.com/CBirkbeck/AINTLIB, Apache-2.0), pinned at 513e83879e2f8cbc626eb9e04d660e92be16ccba: HasseWeil/Basic.lean, private declarations max_natDegree_num_denom_mulByInt and finrank_ratFunc_mulByInt. Adapted rather than ported: that version assumes n ≠ 0.

@[simp]

theorem WeierstrassCurve.finrank_adjoin_Φ_div_ΨSq {F : Type u_1} [Field F] (W : WeierstrassCurve F) (n : ℤ) (hΔ : n ≠ 0 → W.Δ ≠ 0) : Module.finrank (↥F⟮(algebraMap (Polynomial F) (RatFunc F)) (W.Φ n) / (algebraMap (Polynomial F) (RatFunc F)) (W.ΨSq n)⟯) (RatFunc F) = n.natAbs ^ 2

Φₙ / ΨSqₙ has degree n²: adjoining it to F inside the rational function field leaves an extension of dimension n². For n ≠ 0 this is the statement that the x-coordinate map of [n] is a rational map of degree n² — the arithmetic half of deg [n] = n².

Nonsingularity is assumed only where it is used. At n = 0 the quotient is not a coordinate of anything — [0] sends every point to infinity, and ΨSq₀ vanishes, making the quotient the junk value 0 — and the equality holds there for a singular W too, as one between two zeros: F⟮0⟯ is ⊥ and F(x) is not finite-dimensional over F, so the finrank is 0 by convention, while (0 : ℤ).natAbs ^ 2 is 0 as well. TauCeti.RatFunc.finrank_adjoin_X_pow reads the same way at n = 0, for the same reason.