The translation action of the point group on the function field #
For a point P of an elliptic curve W over a field F, the translation τ_P : Q ↦ Q + P is an
automorphism of the curve — of the curve, not of the elliptic curve: it does not fix the point at
infinity unless P = O, so it is not an isogeny. What it does induce is an F-algebra
automorphism τ_P^* of the function field F(W), and P ↦ τ_P^* is a faithful action of the
point group on F(W). This file constructs that action.
The construction runs through the generic point g of
TauCeti/AlgebraicGeometry/EllipticCurve/Affine/FunctionField/GenericPoint/Basic.lean.
Translating a function by P is evaluating it at g + P, so the pullback of τ_P on the affine
coordinate ring is CoordinateRing.evalAlgHom at the coordinates of the translate g + P_{F(W)},
and the composition law is the associativity of the point group: applying τ_Q^* to a coordinate
of g + P moves the generic point to g + Q, hence the pair to g + P + Q.
Two facts make the construction go through, and both come down to the transcendence of the
coordinate function x. First, g + P is never the point at infinity, since otherwise g would
be a constant point. Second, its x-coordinate is again transcendental: were it algebraic, the
Weierstrass equation — monic of degree 2 in y — would make its y-coordinate algebraic too, so
g + P would be a point over the relative algebraic closure of F in F(W), and subtracting the
constant point P would put g there as well. Transcendence is what makes the evaluation map
injective (CoordinateRing.algHom_injective) and so extendable to the fraction field.
Main definitions #
WeierstrassCurve.Affine.translatedGenericPoint: the translateg + Pof the generic point.WeierstrassCurve.Affine.translation: the automorphismτ_P^*of the function field.WeierstrassCurve.Affine.translationHom: the action, as a monoid homomorphism out ofMultiplicative (W⁄F).Point.
Main results #
WeierstrassCurve.Affine.translation_zeroandWeierstrassCurve.Affine.translation_add: the action laws,τ_O^* = 1andτ_{P + Q}^* = τ_P^* ≫ τ_Q^*.WeierstrassCurve.Affine.translation_eq_one_iffandWeierstrassCurve.Affine.translation_injectiveandWeierstrassCurve.Affine.translationHom_injective: the action is faithful.WeierstrassCurve.Affine.translation_apply_genericX_someandWeierstrassCurve.Affine.translation_apply_genericY_some: for an affinePthe two coordinate functions are moved by the Weierstrass addition formulas, which is what identifies this automorphism with the pullback ofτ_P.
[DecidableEq F] is Mathlib's hypothesis for the group law on Affine.Point, and it is inherited
here; the function field gets its own instance from it, so the points of W⁄F(W) are available
with no further assumption.
Roadmap #
TauCetiRoadmap/EllipticCurves/README.md, Layer 0.5, third milestone: "function-field
pullbacks of the translations τ_P, with the action and composition laws". Layer 1's dual-isogeny
milestone consumes them — "Kˢᵉᵖ(W₁)/φ^*Kˢᵉᵖ(W₂) is Galois with group ker φ(Kˢᵉᵖ) acting by
translations" — and so does the place-free fibre count of Layer 1, where "translation moves the
kernel fibre onto one".
References #
- J. Silverman, The Arithmetic of Elliptic Curves, II.2, III.4.
Provenance #
Not a port: none of the pinned sources builds the translation action. The pullback is manufactured
from Mathlib's Affine.Point group law rather than from the addition formulas directly, so the
composition law is the associativity Mathlib already proved.
The translate of the generic point of W by a point P.
Equations
Instances For
The translated generic point is the generic point plus the base change of P.
A translate of the generic point is never the point at infinity: the coordinate x is
transcendental, so the generic point is not the negative of a constant point.
The translation of the function field by a point P. It is the pullback of the
translation τ_P : Q ↦ Q + P of the curve: on the affine coordinate ring it is evaluation at the
translate of the generic point by P, and its inverse is the translation by -P.
Equations
Instances For
Translation of a regular function is evaluation at the translated generic point.
Translation carries the generic point to the translated generic point.
Translation by Q carries the translate by P to the translate by P + Q.
The translation by the point at infinity is the identity.
The composition law of the translations. Translating by P and then by Q is
translating by P + Q; on function fields the pullbacks compose in that same order, the point
group being commutative.
The translation action of the point group on the function field.
Equations
- W.translationHom = { toFun := fun (P : Multiplicative (WeierstrassCurve.toAffine (W.baseChange F)).Point) => W.translation (Multiplicative.toAdd P), map_one' := ⋯, map_mul' := ⋯ }
Instances For
The translation moves the coordinate x to the x-coordinate of the translate of the
generic point: this is what makes translation the pullback of τ_P.
The translation moves the coordinate y to the y-coordinate of the translate of the
generic point.
The translation action is faithful: only the point at infinity acts trivially. Both coordinates of the translate of the generic point being unmoved makes the translate the generic point itself.
Distinct points induce distinct translations of the function field: the action of the
point group is faithful, translation W P = translation W Q forcing P = Q.
The translation action homomorphism is injective: the packaged action is faithful.
The translation of the coordinate x by an affine point, read off the addition
formulas: the generic point and a constant point are never in the degenerate case, the coordinate
x taking no constant value.
The translation of the coordinate y by an affine point, read off the addition
formulas.