Translations move the places of points

Let W be an elliptic curve over a field F. The automorphism group of F(W) over F acts on the places of F(W) (TauCeti.Place.instMulActionAlgEquiv), and the translation τ_P^* is such an automorphism. It moves the place of a point Q to the place of Q - P: the function τ_P^* f takes at Q the value f takes at Q + P, and the place σ • v is the one at which σ f behaves as f does at v. Through the equivariance of principal divisors (TauCeti.Divisor.principal_smul) this computes the divisor of a translated function from the divisor of the function, which is what the divisor calculus of the Weil pairing needs.

Main results

• WeierstrassCurve.Affine.translation_smul_pointEquivDegreeOnePlace: τ_P^* carries the place of Q to the place of Q - P.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.3, III.8.

@[simp]

theorem WeierstrassCurve.Affine.translation_smul_pointEquivDegreeOnePlace {F : Type u_1} [Field F] [DecidableEq F] (W : Affine F) [WeierstrassCurve.IsElliptic W] (P Q : W.Point) : W.translation ((Point.equivBaseChangeSelf W) P) • ↑(W.pointEquivDegreeOnePlace Q) = ↑(W.pointEquivDegreeOnePlace (Q - P))

The translation by P carries the place of Q to the place of Q - P: τ_P^* f has at Q the behaviour of f at Q + P.