The tautological point is the generic point, pushed along the pullback

The tautological point of an isogeny φ : W₁ ⟶ W₂ is the point of W₂ over F(W₁) whose coordinates are the pullbacks of the two coordinate functions of W₂. Those pullbacks are the images of the generic coordinates of W₂ under the function-field map φ^*, so the tautological point is nothing but the generic point of W₂ transported along φ^* by Mathlib's WeierstrassCurve.Affine.Point.map.

The transport is an AddMonoidHom and is functorial, so the tautological point of a composite ψ ∘ φ is the tautological point of ψ transported along φ^*. This expresses a composite of pullbacks as a statement in the group W₃⁄F(W₁), which is how [m] ∘ [n] = [m n] is proved in MulByInt/Comp.lean.

Main results

• TauCeti.Isogeny.tautologicalPoint_eq_map_genericPoint: the tautological point of φ is the generic point of W₂ transported along φ^*.
• TauCeti.Isogeny.tautologicalPoint_comp: the tautological point of a composite ψ ∘ φ is the tautological point of ψ transported along φ^*.

References

• J. Silverman, The Arithmetic of Elliptic Curves, II.2.

@[simp]

theorem TauCeti.Isogeny.tautologicalPoint_eq_map_genericPoint {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (φ : Isogeny W₁ W₂) : φ.pullback.tautologicalPoint = (WeierstrassCurve.Affine.Point.map φ.fieldPullback) W₂.genericPoint

The tautological point is the generic point transported along the pullback.

theorem TauCeti.Isogeny.tautologicalPoint_comp {F : Type u_1} [Field F] {W₁ W₂ W₃ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₃] (ψ : Isogeny W₂ W₃) (φ : Isogeny W₁ W₂) : (ψ.comp φ).pullback.tautologicalPoint = (WeierstrassCurve.Affine.Point.map φ.fieldPullback) ψ.pullback.tautologicalPoint

The tautological point of a composite is the tautological point of the outer isogeny transported along the function-field pullback of the inner isogeny.