Coordinates and constructor elimination for affine points

WeierstrassCurve.Affine.Point is a two-constructor inductive type: the point at infinity, and an affine point together with a nonsingularity certificate. Ruling out the first constructor and naming the data of the second is a step that recurs wherever a point is known to be nonzero. This file also supplies total coordinate accessors, junk-valued at the point at infinity, so downstream definitions can read both coordinates without embedding a case split.

The existential form reads best when the point is a compound term such as n • P: obtain names the coordinates, the nonsingularity certificate and the identifying equation in one line, with no separate generalisation to arrange. The accessor form is useful when the coordinates must occur in a definition, such as evaluation at a translated generic point.

Most coordinate reconstruction results assume the point is nonzero. The descent criterion exists_map_eq_iff handles infinity separately: both accessors are 0 there, and infinity descends along every field embedding. Nothing here needs ellipticity. The map lemmas need field hypotheses only because Mathlib's Point.map does.

Main definitions

• WeierstrassCurve.Affine.Point.xCoord and WeierstrassCurve.Affine.Point.yCoord: the two affine coordinates, both 0 at infinity.

Main results

• WeierstrassCurve.Affine.Point.exists_eq_some_of_ne_zero: a nonzero affine point is .some, in a form that applies to a compound point.
• WeierstrassCurve.Affine.Point.nonsingular_coords and WeierstrassCurve.Affine.Point.some_coords: a nonzero point is .some of its accessors.
• WeierstrassCurve.Affine.Point.eq_of_coords: nonzero points with equal coordinates are equal.
• WeierstrassCurve.Affine.Point.xCoord_map and WeierstrassCurve.Affine.Point.yCoord_map: the accessors commute with Point.map.
• WeierstrassCurve.Affine.Point.exists_map_eq_iff: a point descends along a field embedding exactly when both coordinates do.
• WeierstrassCurve.Affine.Point.cast_zero and WeierstrassCurve.Affine.Point.cast_some: transport along an equality of curves, as in AddEquiv.cast and Equiv.cast, fixes the point at infinity and keeps the coordinates of a point.

The coordinate accessors support TauCetiRoadmap/EllipticCurves/README.md, Layer 0.5, whose translation-action milestone evaluates functions at translates of the generic point.

Provenance

Not a port: Mathlib carries Point.xRep, the projective representative of the x-coordinate map to ℙ¹, but that object intentionally identifies ±P and records no y-coordinate.

theorem WeierstrassCurve.Affine.Point.exists_eq_some_of_ne_zero {F : Type u_1} [CommRing F] {E : WeierstrassCurve F} {P : E.toAffine.Point} (hP : P ≠ 0) : ∃ (x : F) (y : F) (hns : E.toAffine.Nonsingular x y), P = some x y hns

A nonzero affine point is .some. The case split on Affine.Point's two constructors, packaged as an existential: one obtain yields the coordinates, the nonsingularity certificate, and the equation identifying the point with .some of them — the last being what consumers go on to rewrite with.

def WeierstrassCurve.Affine.Point.xCoord {R : Type u_2} [CommRing R] {W : Affine R} : W.Point → R

The x-coordinate of a point, taken to be 0 at the point at infinity.

Equations

• WeierstrassCurve.Affine.Point.zero.xCoord = 0
• (WeierstrassCurve.Affine.Point.some x_1 y h).xCoord = x_1

def WeierstrassCurve.Affine.Point.yCoord {R : Type u_2} [CommRing R] {W : Affine R} : W.Point → R

The y-coordinate of a point, taken to be 0 at the point at infinity.

Equations

• WeierstrassCurve.Affine.Point.zero.yCoord = 0
• (WeierstrassCurve.Affine.Point.some x_1 y h).yCoord = y

@[simp]

theorem WeierstrassCurve.Affine.Point.xCoord_zero {R : Type u_2} [CommRing R] {W : Affine R} : xCoord 0 = 0

@[simp]

theorem WeierstrassCurve.Affine.Point.yCoord_zero {R : Type u_2} [CommRing R] {W : Affine R} : yCoord 0 = 0

@[simp]

theorem WeierstrassCurve.Affine.Point.xCoord_some {R : Type u_2} [CommRing R] {W : Affine R} {x y : R} (h : W.Nonsingular x y) : (some x y h).xCoord = x

@[simp]

theorem WeierstrassCurve.Affine.Point.yCoord_some {R : Type u_2} [CommRing R] {W : Affine R} {x y : R} (h : W.Nonsingular x y) : (some x y h).yCoord = y

theorem WeierstrassCurve.Affine.Point.nonsingular_coords {R : Type u_2} [CommRing R] {W : Affine R} {P : W.Point} (hP : P ≠ 0) : W.Nonsingular P.xCoord P.yCoord

The coordinates of a nonzero point are a nonsingular solution of the equation.

theorem WeierstrassCurve.Affine.Point.some_coords {R : Type u_2} [CommRing R] {W : Affine R} {P : W.Point} (hP : P ≠ 0) : some P.xCoord P.yCoord ⋯ = P

A nonzero point is Point.some of its two coordinates.

theorem WeierstrassCurve.Affine.Point.eq_of_coords {R : Type u_2} [CommRing R] {W : Affine R} {P Q : W.Point} (hP : P ≠ 0) (hQ : Q ≠ 0) (hx : P.xCoord = Q.xCoord) (hy : P.yCoord = Q.yCoord) : P = Q

Two nonzero points with the same two affine coordinates are equal.

@[simp]

theorem WeierstrassCurve.Affine.Point.xCoord_neg {R : Type u_2} [CommRing R] {W : Affine R} (P : W.Point) : (-P).xCoord = P.xCoord

@[simp]

theorem WeierstrassCurve.Affine.Point.yCoord_neg {R : Type u_2} [CommRing R] {W : Affine R} {P : W.Point} (hP : P ≠ 0) : (-P).yCoord = W.negY P.xCoord P.yCoord

The y-coordinate of the negation of a nonzero point.

@[simp]

theorem WeierstrassCurve.Affine.Point.xCoord_map {R : Type u_2} [CommRing R] {W : Affine R} {S : Type u_3} {F : Type u_4} {K : Type u_5} [CommRing S] [Field F] [Field K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] [DecidableEq F] [DecidableEq K] (f : F →ₐ[S] K) (P : (toAffine (W.baseChange F)).Point) : ((map f) P).xCoord = f P.xCoord

The x-coordinate commutes with Point.map. The point at infinity needs no exception: both sides are 0 there.

@[simp]

theorem WeierstrassCurve.Affine.Point.yCoord_map {R : Type u_2} [CommRing R] {W : Affine R} {S : Type u_3} {F : Type u_4} {K : Type u_5} [CommRing S] [Field F] [Field K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] [DecidableEq F] [DecidableEq K] (f : F →ₐ[S] K) (P : (toAffine (W.baseChange F)).Point) : ((map f) P).yCoord = f P.yCoord

The y-coordinate commutes with Point.map.

@[simp]

theorem WeierstrassCurve.Affine.Point.exists_map_eq_iff {R : Type u_2} [CommRing R] {W : Affine R} {S : Type u_3} {F : Type u_4} {K : Type u_5} [CommRing S] [Field F] [Field K] [Algebra R S] [Algebra R F] [Algebra S F] [IsScalarTower R S F] [Algebra R K] [Algebra S K] [IsScalarTower R S K] [DecidableEq F] [DecidableEq K] (P : (toAffine (W.baseChange K)).Point) (f : F →ₐ[S] K) : (∃ (Q : (toAffine (W.baseChange F)).Point), (map f) Q = P) ↔ P.xCoord ∈ Set.range ⇑f ∧ P.yCoord ∈ Set.range ⇑f

A point descends along a field embedding exactly when both coordinates lie in its image. The point at infinity also satisfies the criterion, since its coordinate accessors are zero.

theorem WeierstrassCurve.Affine.Point.cast_zero {R : Type u_6} [CommRing R] {V V' : WeierstrassCurve R} (h : V = V') : cast ⋯ 0 = 0

Transport of affine points along an equality of Weierstrass curves fixes the point at infinity. Mathlib's AddEquiv.cast and Equiv.cast both reduce to this cast.

theorem WeierstrassCurve.Affine.Point.cast_some {R : Type u_6} [CommRing R] {V V' : WeierstrassCurve R} (h : V = V') {x y : R} (hns : V.toAffine.Nonsingular x y) : cast ⋯ (some x y hns) = some x y ⋯

Transport of affine points along an equality of Weierstrass curves keeps the coordinates of a point. Mathlib's AddEquiv.cast and Equiv.cast both reduce to this cast. It is used by the variable-change and quadratic-twist point isomorphisms and by the base-change point map WeierstrassCurve.Affine.pointMap (MordellWeil/LocalCondition.lean).