Weierstrass curves

DefinitionCoordinate map of a Weierstrass variable change#✓fully proved

For a variable change \(C = (u, r, s, t)\) over a field \(F\), with \(u \in F^\times\) and \(r, s, t \in F\), the affine coordinate map of \(C\) sends \((x, y) \in F^2\) to \((u^2 x + r,\ u^3 y + u^2 s x + t)\).

def mapAffineCoordinates (C : VariableChange F) (xy : F × F) : F × F :=
  (C.u ^ 2 * xy.1 + C.r,
    C.u ^ 3 * xy.2 + C.u ^ 2 * C.s * xy.1 + C.t)

Used by 3

Used byVariable changes act bijectively on affine coordinates · Variable changes biject affine solutions · Variable changes transform the Weierstrass equation

DefinitionVariable changes act bijectively on affine coordinates#✓fully proved

For a variable change \(C = (u, r, s, t)\) over a field \(F\), the map \((x, y) \mapsto (u^2 x + r,\ u^3 y + u^2 s x + t)\) is a bijection \(F^2 \to F^2\), whose inverse is the corresponding map of the inverse variable change \(C^{-1}\).

def affineCoordinatesEquiv (C : VariableChange F) : F × F ≃ F × F where
  toFun := mapAffineCoordinates C
  invFun := mapAffineCoordinates C⁻¹
  left_inv := mapAffineCoordinates_inv_apply C
  right_inv := mapAffineCoordinates_apply_inv C

Uses 1

Statement usesCoordinate map of a Weierstrass variable change

TheoremVariable changes transform the Weierstrass equation#✓fully proved

Let \(W\) be a Weierstrass curve over a field \(F\), let \(C = (u, r, s, t)\) be a variable change and let \(C \cdot W\) be the transformed curve. A pair \((x, y) \in F^2\) satisfies the Weierstrass equation of \(C \cdot W\) if and only if \((u^2 x + r,\ u^3 y + u^2 s x + t)\) satisfies the Weierstrass equation of \(W\).

theorem equation_mapAffineCoordinates_iff (C : VariableChange F) (W : WeierstrassCurve F)
    (xy : F × F) :
    (C • W).toAffine.Equation xy.1 xy.2 ↔
      W.toAffine.Equation (mapAffineCoordinates C xy).1
        (mapAffineCoordinates C xy).2

Uses 1 · Used by 1

Statement usesCoordinate map of a Weierstrass variable change

Used byVariable changes biject affine solutions

DefinitionVariable changes biject affine solutions#✓fully proved

Let \(W\) be a Weierstrass curve over a field \(F\), let \(C = (u, r, s, t)\) be a variable change and let \(C \cdot W\) be the transformed curve. The map \((x, y) \mapsto (u^2 x + r,\ u^3 y + u^2 s x + t)\) is a bijection from the solutions \((x, y) \in F^2\) of the Weierstrass equation of \(C \cdot W\) onto the solutions in \(F^2\) of the Weierstrass equation of \(W\); its inverse is the corresponding map of \(C^{-1}\).

WeierstrassCurve.VariableChange.affineEquationEquiv · 16 lines

def affineEquationEquiv (C : VariableChange F) (W : WeierstrassCurve F) :
    {xy : F × F // (C • W).toAffine.Equation xy.1 xy.2} ≃
      {xy : F × F // W.toAffine.Equation xy.1 xy.2} where
  toFun xy :=
    ⟨mapAffineCoordinates C xy.1,
      (equation_mapAffineCoordinates_iff C W xy.1).mp xy.2⟩
  invFun xy :=
    ⟨mapAffineCoordinates C⁻¹ xy.1, by
      rw [equation_mapAffineCoordinates_iff]
      simpa using xy.2⟩
  left_inv xy := by
    apply Subtype.ext
    exact mapAffineCoordinates_inv_apply C xy.1
  right_inv xy := by
    apply Subtype.ext
    exact mapAffineCoordinates_apply_inv C xy.1

Uses 2 · Used by 1

Statement usesVariable changes transform the Weierstrass equation · Coordinate map of a Weierstrass variable change

Used byVariable changes biject rational points

DefinitionVariable changes biject rational points#✓fully proved

Let \(W\) be an elliptic Weierstrass curve over a field \(F\), let \(C = (u, r, s, t)\) be a variable change and let \(C \cdot W\) be the transformed curve. There is a bijection from the rational points of \(C \cdot W\) to the rational points of \(W\), where in both cases the point at infinity is included; it sends the point at infinity to the point at infinity and an affine point \((x, y)\) to \((u^2 x + r,\ u^3 y + u^2 s x + t)\).

noncomputable def pointEquiv (C : VariableChange F) (W : WeierstrassCurve F)
    [W.IsElliptic] :
    (C • W).toAffine.Point ≃ W.toAffine.Point :=
  (C • W).toAffine.pointEquiv |>.trans
    ((affineEquationEquiv C W).optionCongr.trans W.toAffine.pointEquiv.symm)

Uses 1 · Used by 1

Statement usesVariable changes biject affine solutions

Used byVariable changes preserve the point count

TheoremVariable changes preserve the point count#✓fully proved

Let \(W\) be an elliptic Weierstrass curve over a finite field \(F\), let \(C\) be a variable change and let \(C \cdot W\) be the transformed curve. Then \(C \cdot W\) and \(W\) have the same number of rational points.

theorem natCard_point_eq [Finite F] (C : VariableChange F) (W : WeierstrassCurve F)
    [W.IsElliptic] :
    Nat.card ((C • W).toAffine.Point) = Nat.card W.toAffine.Point

Uses 1 · Used by 1

Proof usesVariable changes biject rational points

Used byHasse bound

TheoremThe ideal of a point on a Weierstrass curve is nonzero#✓fully proved

The ideal generated by X - x and Y - y is nonzero.

theorem XYIdeal_ne_bot {R : Type*} [CommRing R] [Nontrivial R] {W : Affine R} (x : R)
    (y : R[X]) : XYIdeal W x y ≠ ⊥

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.