Definitions/Def_WeierstrassCurve_RatPointMap_probe.lean

Fix fields F and k, a ring homomorphism f : F \to k, and a Weierstrass curve W_0 over F, given by its coefficients a_1,a_2,a_3,a_4,a_6. Mathlib's base change WeierstrassCurve.map produces the Weierstrass curve W_0.\mathrm{map}\,f over k whose coefficients are the images f(a_i). The module defines ratPointMap, the map from the set of affine points of W_0 (the Mathlib type W₀.toAffine.Point, whose elements are either the point at infinity .zero or a pair (x,y) of coordinates in F together with a proof that (x,y) is a nonsingular point of the affine equation) to the affine points of W_0.\mathrm{map}\,f. It is defined by cases: the point at infinity goes to the point at infinity, and a point with coordinates (x,y) goes to the point with coordinates (f(x), f(y)). That the image pair is again a nonsingular solution of the transported equation is supplied by Mathlib's WeierstrassCurve.Affine.map_nonsingular, applied with the injectivity of f (automatic for a ring homomorphism out of a field). The definition is a map of underlying point sets only; no group-homomorphism property is asserted here.

Alongside it, a small auxiliary congruence statement some_congr records that for an affine Weierstrass curve V over k and coordinates x_1,y_1,x_2,y_2 in k with x_1 = x_2 and y_1 = y_2, the points Point.some x₁ y₁ h₁ and Point.some x₂ y₂ h₂ are equal, for any two nonsingularity proofs h_1, h_2: the point depends only on its coordinates, the proof component being irrelevant.