Adding coordinate pullbacks

A coordinate pullback W₂.CoordinateRing →ₐ[F] W₁.FunctionField is the same thing as a point of W₂ over F(W₁) — its tautological point — so two of them can be added by adding those points in the group law of W₂⁄F(W₁) and evaluating the coordinate ring at the result. This is the Weierstrass addition law read on function fields, taken from Mathlib's group structure on points rather than from the rational formulas directly.

The sum of two points may be the point at infinity, which is not the tautological point of anything, so add takes that exclusion as a hypothesis; on the hom carrier, where a zero element is available, that case is the zero map (Isogeny/Hom/Add.lean). The sum of two pointed pullbacks whose tautological points do not cancel is pointed again (mapsInfinity_add), so the sum of two isogenies is an isogeny.

Main definitions

• TauCeti.CoordinatePullback.add: the sum of two coordinate pullbacks whose tautological points do not cancel.

Main results

• TauCeti.CoordinatePullback.add_of_X and TauCeti.CoordinatePullback.add_root: the sum's values on the two coordinate functions of W₂.
• TauCeti.CoordinatePullback.tautologicalPoint_add: the defining property — the tautological point of the sum is the sum of the tautological points.
• TauCeti.CoordinatePullback.eq_add_of_tautologicalPoint_eq: that property characterises the sum.
• TauCeti.CoordinatePullback.mapsInfinity_add: the sum of two pointed pullbacks whose tautological points do not cancel is pointed.
• TauCeti.CoordinatePullback.add_comm and TauCeti.CoordinatePullback.add_assoc: addition is commutative and associative where it is defined.

Provenance

The same construction is formalised in the AINTLIB HasseWeil project (Chris Birkbeck), Apache-2.0, HasseWeil/AdditionPullback.lean at commit 513e83879e2f8cbc626eb9e04d660e92be16ccba, declarations addSlope, addPullback_x, addPullback_y, addCoordAlgHomPair and addIsog, which build the sum from the explicit rational formulas. Nothing here is adapted from it: that construction assumes the induced map on points as data, and its case analysis on the formulas is what Mathlib's AddCommGroup on points already discharges, so the declarations below are written against the point group instead.

noncomputable def TauCeti.CoordinatePullback.add {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q : CoordinatePullback W₁ W₂) (h : p.tautologicalPoint + q.tautologicalPoint ≠ 0) : CoordinatePullback W₁ W₂

The sum of two coordinate pullbacks, when their tautological points do not cancel: evaluation of the coordinate ring of W₂ at the sum of those points.

Equations

• p.add q h = WeierstrassCurve.Affine.CoordinateRing.evalAlgHom ⋯

@[simp]

theorem TauCeti.CoordinatePullback.add_of_X {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q : CoordinatePullback W₁ W₂) (h : p.tautologicalPoint + q.tautologicalPoint ≠ 0) : (p.add q h) ((AdjoinRoot.of W₂.polynomial) Polynomial.X) = (p.tautologicalPoint + q.tautologicalPoint).xCoord

The sum sends the coordinate function x of W₂ to the x-coordinate of the sum point.

@[simp]

theorem TauCeti.CoordinatePullback.add_root {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q : CoordinatePullback W₁ W₂) (h : p.tautologicalPoint + q.tautologicalPoint ≠ 0) : (p.add q h) (AdjoinRoot.root W₂.polynomial) = (p.tautologicalPoint + q.tautologicalPoint).yCoord

The sum sends the coordinate function y of W₂ to the y-coordinate of the sum point.

@[simp]

theorem TauCeti.CoordinatePullback.tautologicalPoint_add {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q : CoordinatePullback W₁ W₂) (h : p.tautologicalPoint + q.tautologicalPoint ≠ 0) : (p.add q h).tautologicalPoint = p.tautologicalPoint + q.tautologicalPoint

The defining property of the sum: its tautological point is the sum of the tautological points.

theorem TauCeti.CoordinatePullback.eq_add_of_tautologicalPoint_eq {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] {p q r : CoordinatePullback W₁ W₂} (hr : r.tautologicalPoint = p.tautologicalPoint + q.tautologicalPoint) : r = p.add q ⋯

The defining property characterises the sum: a pullback whose tautological point is the sum of two others is their sum.

theorem TauCeti.CoordinatePullback.add_comm {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q : CoordinatePullback W₁ W₂) (h : p.tautologicalPoint + q.tautologicalPoint ≠ 0) : p.add q h = q.add p ⋯

Addition of coordinate pullbacks is commutative where it is defined.

theorem TauCeti.CoordinatePullback.add_assoc {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q r : CoordinatePullback W₁ W₂) (hpq : p.tautologicalPoint + q.tautologicalPoint ≠ 0) (hqr : q.tautologicalPoint + r.tautologicalPoint ≠ 0) (h : (p.add q hpq).tautologicalPoint + r.tautologicalPoint ≠ 0) : (p.add q hpq).add r h = p.add (q.add r hqr) ⋯

Addition of coordinate pullbacks is associative where both regroupings are defined.

theorem TauCeti.CoordinatePullback.mapsInfinity_add {F : Type u_1} [Field F] {W₁ W₂ : WeierstrassCurve.Affine F} [WeierstrassCurve.IsElliptic W₂] (p q : CoordinatePullback W₁ W₂) (hp : p.MapsInfinity) (hq : q.MapsInfinity) (h : p.tautologicalPoint + q.tautologicalPoint ≠ 0) : (p.add q h).MapsInfinity

The sum of two pointed coordinate pullbacks whose tautological points do not cancel is pointed.