Isomorphism of point groups induced by a change of variables

This file is ported from Michael Stoll's Apache-2.0 EllipticCurves project at commit 3f8c39c0fc4c0fd0a40e693aa2a9bbda08d9ee1f.

The derivative-transport and singular-cubic nonsingular-locus equivalence are local extensions. They generalize the ported point equivalence beyond elliptic equations while retaining the original admissible change-of-variables formulas and attribution.

Mathlib's affine Point API provides the group homomorphism induced by a change of the base field for a fixed Weierstrass curve, but not the isomorphism of Mordell--Weil groups induced by an admissible change of variables between two different curves. For C : WeierstrassCurve.VariableChange F, the admissible change

(x, y) ↦ (u²x + r, u³y + u²sx + t)

gives the group isomorphism WeierstrassCurve.Affine.Point.equivVariableChange : (C • W).Point ≃+ W.Point. Its inverse is the explicit change of variables C⁻¹.

Transformation of the group-law formulae under a change of variables

theorem WeierstrassCurve.Affine.variableChange_negY {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x y : F) : W.toAffine.negY (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) = ↑C.u ^ 3 * (C • W).toAffine.negY x y + ↑C.u ^ 2 * C.s * x + C.t

theorem WeierstrassCurve.Affine.variableChange_negY_ne {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) {x₁ x₂ y₁ y₂ : F} (hxy : ¬(x₁ = x₂ ∧ y₁ = (C • W).toAffine.negY x₂ y₂)) : ¬(↑C.u ^ 2 * x₁ + C.r = ↑C.u ^ 2 * x₂ + C.r ∧ ↑C.u ^ 3 * y₁ + ↑C.u ^ 2 * C.s * x₁ + C.t = W.toAffine.negY (↑C.u ^ 2 * x₂ + C.r) (↑C.u ^ 3 * y₂ + ↑C.u ^ 2 * C.s * x₂ + C.t))

The image of a pair of points under the change of variables satisfies the y₁ = -y₂ degeneracy condition only if the original pair does.

theorem WeierstrassCurve.Affine.variableChange_addX {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x₁ x₂ ℓ : F) : W.toAffine.addX (↑C.u ^ 2 * x₁ + C.r) (↑C.u ^ 2 * x₂ + C.r) (↑C.u * ℓ + C.s) = ↑C.u ^ 2 * (C • W).toAffine.addX x₁ x₂ ℓ + C.r

theorem WeierstrassCurve.Affine.variableChange_negAddY {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x₁ x₂ y₁ ℓ : F) : W.toAffine.negAddY (↑C.u ^ 2 * x₁ + C.r) (↑C.u ^ 2 * x₂ + C.r) (↑C.u ^ 3 * y₁ + ↑C.u ^ 2 * C.s * x₁ + C.t) (↑C.u * ℓ + C.s) = ↑C.u ^ 3 * (C • W).toAffine.negAddY x₁ x₂ y₁ ℓ + ↑C.u ^ 2 * C.s * (C • W).toAffine.addX x₁ x₂ ℓ + C.t

theorem WeierstrassCurve.Affine.variableChange_addY {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x₁ x₂ y₁ ℓ : F) : W.toAffine.addY (↑C.u ^ 2 * x₁ + C.r) (↑C.u ^ 2 * x₂ + C.r) (↑C.u ^ 3 * y₁ + ↑C.u ^ 2 * C.s * x₁ + C.t) (↑C.u * ℓ + C.s) = ↑C.u ^ 3 * (C • W).toAffine.addY x₁ x₂ y₁ ℓ + ↑C.u ^ 2 * C.s * (C • W).toAffine.addX x₁ x₂ ℓ + C.t

theorem WeierstrassCurve.Affine.variableChange_slope {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) [DecidableEq F] {x₁ x₂ y₁ y₂ : F} (h₁ : (C • W).toAffine.Equation x₁ y₁) (h₂ : (C • W).toAffine.Equation x₂ y₂) (hxy : ¬(x₁ = x₂ ∧ y₁ = (C • W).toAffine.negY x₂ y₂)) : W.toAffine.slope (↑C.u ^ 2 * x₁ + C.r) (↑C.u ^ 2 * x₂ + C.r) (↑C.u ^ 3 * y₁ + ↑C.u ^ 2 * C.s * x₁ + C.t) (↑C.u ^ 3 * y₂ + ↑C.u ^ 2 * C.s * x₂ + C.t) = ↑C.u * (C • W).toAffine.slope x₁ x₂ y₁ y₂ + C.s

theorem WeierstrassCurve.Affine.variableChange_equation {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x y : F) : W.toAffine.Equation (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) ↔ (C • W).toAffine.Equation x y

A point (x, y) lies on C • W if and only if (u²x + r, u³y + u²sx + t) lies on W.

theorem WeierstrassCurve.Affine.variableChange_polynomialY {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x y : F) : Polynomial.evalEval (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) W.toAffine.polynomialY = ↑C.u ^ 3 * Polynomial.evalEval x y (C • W).toAffine.polynomialY

The Y-derivative of a Weierstrass equation under an admissible change of variables. This formula does not require either equation to be elliptic.

theorem WeierstrassCurve.Affine.variableChange_polynomialX {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x y : F) : Polynomial.evalEval (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) W.toAffine.polynomialX = ↑C.u ^ 4 * Polynomial.evalEval x y (C • W).toAffine.polynomialX - C.s * (↑C.u ^ 3 * Polynomial.evalEval x y (C • W).toAffine.polynomialY)

The X-derivative of a Weierstrass equation under an admissible change of variables. The correction term is the chain-rule contribution from the sx term in the new Y coordinate. This formula does not require either equation to be elliptic.

theorem WeierstrassCurve.Affine.variableChange_nonsingular {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) (x y : F) : W.toAffine.Nonsingular (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) ↔ (C • W).toAffine.Nonsingular x y

An admissible change of variables identifies the nonsingular loci even when the common Weierstrass cubic is singular.

The induced isomorphism of point groups

def WeierstrassCurve.Affine.Point.mapVariableChangeFun {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) : (C • W).toAffine.Point → W.toAffine.Point

The underlying point map of the change of variables, sending 0 to 0.

Equations

• One or more equations did not get rendered due to their size.
• WeierstrassCurve.Affine.Point.mapVariableChangeFun W C WeierstrassCurve.Affine.Point.zero = WeierstrassCurve.Affine.Point.zero

@[simp]

theorem WeierstrassCurve.Affine.Point.mapVariableChangeFun_zero {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) : mapVariableChangeFun W C 0 = 0

theorem WeierstrassCurve.Affine.Point.mapVariableChangeFun_some {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) {x y : F} (h : (C • W).toAffine.Nonsingular x y) : mapVariableChangeFun W C (some x y h) = some (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) ⋯

theorem WeierstrassCurve.Affine.Point.some_eq_some {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x₁ x₂ y₁ y₂ : F} (hx : x₁ = x₂) (hy : y₁ = y₂) {h₁ : W.toAffine.Nonsingular x₁ y₁} {h₂ : W.toAffine.Nonsingular x₂ y₂} : some x₁ y₁ h₁ = some x₂ y₂ h₂

theorem WeierstrassCurve.Affine.Point.mapVariableChangeFun_injective {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) : Function.Injective (mapVariableChangeFun W C)

def WeierstrassCurve.Affine.Point.equivOfEq {F : Type u_1} [Field F] [DecidableEq F] {V V' : WeierstrassCurve F} (h : V = V') : V.toAffine.Point ≃+ V'.toAffine.Point

Transport of the affine point group along an equality of Weierstrass curves.

Equations

• WeierstrassCurve.Affine.Point.equivOfEq h = h ▸ AddEquiv.refl V.toAffine.Point

@[simp]

theorem WeierstrassCurve.Affine.Point.equivOfEq_some {F : Type u_1} [Field F] [DecidableEq F] {V V' : WeierstrassCurve F} (h : V = V') {x y : F} (hns : V.toAffine.Nonsingular x y) : (equivOfEq h) (some x y hns) = some x y ⋯

def WeierstrassCurve.Affine.Point.mapVariableChange {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) [DecidableEq F] : (C • W).toAffine.Point →+ W.toAffine.Point

The group homomorphism induced by the admissible change of variables.

Equations

• WeierstrassCurve.Affine.Point.mapVariableChange W C = { toFun := WeierstrassCurve.Affine.Point.mapVariableChangeFun W C, map_zero' := ⋯, map_add' := ⋯ }

def WeierstrassCurve.Affine.Point.equivVariableChange {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) [DecidableEq F] : (C • W).toAffine.Point ≃+ W.toAffine.Point

The point-group isomorphism induced by the admissible change of variables.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Affine.Point.equivVariableChange_some {F : Type u_1} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) [DecidableEq F] {x y : F} (h : (C • W).toAffine.Nonsingular x y) : (equivVariableChange W C) (some x y h) = some (↑C.u ^ 2 * x + C.r) (↑C.u ^ 3 * y + ↑C.u ^ 2 * C.s * x + C.t) ⋯