Translations under change of the coefficient field

Let W be a Weierstrass 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 (WeierstrassCurve.Affine.Point.mapAlong), and the function field of W is carried into that of W.map f (WeierstrassCurve.Affine.FunctionField.map). This file proves that the second map intertwines translation by P with translation by f P:

f^* (τ_P^* z) = τ_{f P}^* (f^* z).

Both sides are ring homomorphisms in z, so it suffices to compare them on the constants and on the generic point. On the constants both are f. On the generic point, translation by an affine point is given by the addition formulas, whose coefficients are polynomials in the coefficients of the curve and the coordinates of the point, and f commutes with them.

Main results

• WeierstrassCurve.Affine.FunctionField.map_translation: changing the coefficient field intertwines translation by P with translation by f P.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.4.

theorem WeierstrassCurve.Affine.FunctionField.map_translation {F : Type u_1} {K : Type u_2} [Field F] [Field K] [DecidableEq F] [DecidableEq K] (W : Affine F) [WeierstrassCurve.IsElliptic W] (f : F →+* K) (P : W.Point) (z : W.FunctionField) : (map W f) ((W.translation ((Point.equivBaseChangeSelf W) P)) z) = ((W.map f).translation ((Point.equivBaseChangeSelf (W.map f)) (Point.mapAlong f ⋯ P))) ((map W f) z)

Changing the coefficient field intertwines translation by P with translation by f P: f^* (τ_P^* z) = τ_{f P}^* (f^* z) for every function z on W.