The degree of multiplication by n

deg [n] = n². The degree of an isogeny is the degree of F(W) over the image of its function-field pullback — the pulled-back copy of the target function field. For [n] the target is F(W) again, and the pullback carries the affine coordinate x to Φₙ / ΨSqₙ. That image is pinned down by where the coordinate goes, and DivisionPolynomialTower.lean computes its index as n² by way of the intermediate tower F(Φₙ/ΨSqₙ) ⊆ F(x) ⊆ F(W).

Main results

• TauCeti.Isogeny.fieldPullback_mulByIntIsogeny_X: the function-field pullback of [n] sends the affine coordinate to Φₙ / ΨSqₙ, read in F(x) rather than in the coordinate ring.
• TauCeti.Isogeny.degree_mulByIntIsogeny: deg [n] = n², for an n whose division polynomial does not vanish at the generic point, and TauCeti.Isogeny.degree_mulByIntIsogenyOfNeZero for every n ≠ 0, that hypothesis being discharged from nonsingularity.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.6.4(a).

@[simp]

theorem TauCeti.Isogeny.fieldPullback_mulByIntIsogeny_X {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).fieldPullback ((algebraMap (Polynomial F) W.toAffine.FunctionField) Polynomial.X) = (algebraMap (RatFunc F) W.toAffine.FunctionField) ((algebraMap (Polynomial F) (RatFunc F)) (W.Φ n) / (algebraMap (Polynomial F) (RatFunc F)) (W.ΨSq n))

The pullback of [n] sends the affine coordinate to Φₙ / ΨSqₙ, with the quotient formed in F(x) and then carried into F(W). This is mulByIntX in the shape the degree tower asks for.

@[simp]

theorem TauCeti.Isogeny.degree_mulByIntIsogeny {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : psiFunctionField W n ≠ 0) : (mulByIntIsogeny W hn).degree = n.natAbs ^ 2

deg [n] = n² (Silverman III.6.4(a)). The pullback of [n] sends the affine coordinate to Φₙ / ΨSqₙ, so its image is the field the tower F(Φₙ/ΨSqₙ) ⊆ F(x) ⊆ F(W) measures, of index n².

theorem TauCeti.Isogeny.degree_mulByIntIsogenyOfNeZero {F : Type u_1} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] {n : ℤ} (hn : n ≠ 0) : (mulByIntIsogenyOfNeZero W hn).degree = n.natAbs ^ 2

deg [n] = n² for every n ≠ 0, the non-vanishing hypothesis discharged from nonsingularity as in mulByIntIsogenyOfNeZero.