The tautological point of [n] reduces to n • P

The tautological point of the isogeny [n] is n times the generic point (TauCeti.Isogeny.tautologicalPoint_mulByIntPullback), and the generic point reduces to P at the place of P (WeierstrassCurve.Affine.reductionOfDegreeEqOne_genericPoint). Reduction at a place of degree one is additive, so the tautological point of [n] reduces to n • P there. The tautological point of an isogeny is the isogeny evaluated at the generic point, and its reduction at the place of P is the isogeny evaluated at P; read this way, the statement says that [n] is the group's own multiplication by n.

Main results

• TauCeti.Isogeny.reductionOfDegreeEqOne_tautologicalPoint_mulByIntIsogeny: at the place of P, the tautological point of [n] reduces to n • P.

References

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

theorem TauCeti.Isogeny.reductionOfDegreeEqOne_tautologicalPoint_mulByIntIsogeny {F : Type u_1} [Field F] [DecidableEq F] {W : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W] {n : ℤ} (hn : psiFunctionField W n ≠ 0) (P : W.Point) : (W.reductionOfDegreeEqOne ⋯) (mulByIntIsogeny W hn).pullback.tautologicalPoint = (WeierstrassCurve.Affine.Point.equivBaseChangeSelf W) (n • P)

[n] acts on points as multiplication by n: at the place of P, the tautological point of [n] reduces to n • P.