Translation moves the tautological point of Frobenius by the translating point

Translating by a rational point P sends the generic point g to g + P. The tautological point of the Frobenius isogeny is g pushed along the q-power map, and that map commutes with translation and fixes P, whose coordinates lie in the base field. So the tautological point of Frobenius moves by P as well.

Main results

• TauCeti.Isogeny.map_translation_tautologicalPoint_frobeniusIsogeny: translation by P adds P to the tautological point of Frobenius.

theorem TauCeti.Isogeny.map_translation_tautologicalPoint_frobeniusIsogeny {F : Type u_1} [Field F] [Finite F] [DecidableEq F] (W : WeierstrassCurve.Affine F) [WeierstrassCurve.IsElliptic W] (P : (WeierstrassCurve.toAffine (W.baseChange F)).Point) : (WeierstrassCurve.Affine.Point.map ↑(W.translation P)) (frobeniusIsogeny W).pullback.tautologicalPoint = (frobeniusIsogeny W).pullback.tautologicalPoint + (WeierstrassCurve.Affine.Point.baseChange F W.FunctionField) P

Translation by a rational point adds that point to the tautological point of Frobenius, exactly as it does to the generic point.