Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Projective

Projective coordinates for Weierstrass curves #

This file defines the type of points on a Weierstrass curve as a tuple, consisting of an equivalence class of triples up to scaling by a unit, satisfying a Weierstrass equation with a nonsingular condition.

Mathematical background #

Let W be a Weierstrass curve over a field F. A point on the projective plane is an equivalence class of triples $[x:y:z]$ with coordinates in F such that $(x, y, z) \sim (x', y', z')$ precisely if there is some unit $u$ of F such that $(x, y, z) = (ux', uy', uz')$, with an extra condition that $(x, y, z) \ne (0, 0, 0)$. As described in Mathlib.AlgebraicGeometry.EllipticCurve.Affine, a rational point is a point on the projective plane satisfying a homogeneous Weierstrass equation, and being nonsingular means the partial derivatives $W_X(X, Y, Z)$, $W_Y(X, Y, Z)$, and $W_Z(X, Y, Z)$ do not vanish simultaneously. Note that the vanishing of the Weierstrass equation and its partial derivatives are independent of the representative for $[x:y:z]$, and the nonsingularity condition already implies that $(x, y, z) \ne (0, 0, 0)$, so a nonsingular rational point on W can simply be given by a tuple consisting of $[x:y:z]$ and the nonsingular condition on any representative.

Main definitions #

Main statements #

Implementation notes #

A point representative is implemented as a term P of type Fin 3 → R, which allows for the vector notation ![x, y, z]. However, P is not definitionally equivalent to the expanded vector ![P x, P y, P z], so the auxiliary lemma fin3_def can be used to convert between the two forms. The equivalence of two point representatives P and Q is implemented as an equivalence of orbits of the action of , or equivalently that there is some unit u of R such that P = u • Q. However, u • Q is again not definitionally equal to ![u * Q x, u * Q y, u * Q z], so the auxiliary lemmas smul_fin3 and smul_fin3_ext can be used to convert between the two forms.

References #

[J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags #

elliptic curve, rational point, projective coordinates

Weierstrass curves #

@[reducible, inline]
abbrev WeierstrassCurve.Projective (R : Type u_1) :
Type u_1

An abbreviation for a Weierstrass curve in projective coordinates.

Equations
Instances For
    theorem WeierstrassCurve.Projective.fin3_def {R : Type u} (P : Fin 3R) :
    P = ![P 0, P 1, P 2]
    theorem WeierstrassCurve.Projective.smul_fin3 {R : Type u} [CommRing R] (P : Fin 3R) (u : Rˣ) :
    u P = ![u * P 0, u * P 1, u * P 2]
    theorem WeierstrassCurve.Projective.smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3R) (u : Rˣ) :
    (u P) 0 = u * P 0 (u P) 1 = u * P 1 (u P) 2 = u * P 2

    The equivalence setoid for a point representative.

    Equations
    Instances For
      @[reducible, inline]

      The equivalence class of a point representative.

      Equations
      Instances For
        @[reducible, inline]

        The coercion to a Weierstrass curve in affine coordinates.

        Equations
        • W.toAffine = W
        Instances For

          Equations and nonsingularity #

          The polynomial $W(X, Y, Z) := Y^2Z + a_1XYZ + a_3YZ^2 - (X^3 + a_2X^2Z + a_4XZ^2 + a_6Z^3)$ associated to a Weierstrass curve W over R. This is represented as a term of type MvPolynomial (Fin 3) R, where X 0, X 1, and X 2 represent $X$, $Y$, and $Z$ respectively.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem WeierstrassCurve.Projective.eval_polynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
            (MvPolynomial.eval P) W.polynomial = P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 - (P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3)

            The proposition that a point representative $(x, y, z)$ lies in W. In other words, $W(x, y, z) = 0$.

            Equations
            Instances For
              theorem WeierstrassCurve.Projective.equation_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
              W.Equation P P 1 ^ 2 * P 2 + W.a₁ * P 0 * P 1 * P 2 + W.a₃ * P 1 * P 2 ^ 2 = P 0 ^ 3 + W.a₂ * P 0 ^ 2 * P 2 + W.a₄ * P 0 * P 2 ^ 2 + W.a₆ * P 2 ^ 3
              theorem WeierstrassCurve.Projective.equation_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (Y : R) :
              W.Equation ![0, Y, 0]
              theorem WeierstrassCurve.Projective.equation_some {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (X : R) (Y : R) :
              W.Equation ![X, Y, 1] W.toAffine.Equation X Y
              theorem WeierstrassCurve.Projective.equation_smul_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) (u : Rˣ) :
              W.Equation (u P) W.Equation P

              The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$.

              Equations
              Instances For
                theorem WeierstrassCurve.Projective.polynomialX_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) :
                W.polynomialX = MvPolynomial.C W.a₁ * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C 3 * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W.a₂) * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W.a₄ * MvPolynomial.X 2 ^ 2)
                theorem WeierstrassCurve.Projective.eval_polynomialX {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
                (MvPolynomial.eval P) W.polynomialX = W.a₁ * P 1 * P 2 - (3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2)

                The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$.

                Equations
                Instances For
                  theorem WeierstrassCurve.Projective.polynomialY_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) :
                  W.polynomialY = MvPolynomial.C 2 * MvPolynomial.X 1 * MvPolynomial.X 2 + MvPolynomial.C W.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W.a₃ * MvPolynomial.X 2 ^ 2
                  theorem WeierstrassCurve.Projective.eval_polynomialY {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
                  (MvPolynomial.eval P) W.polynomialY = 2 * P 1 * P 2 + W.a₁ * P 0 * P 2 + W.a₃ * P 2 ^ 2

                  The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$.

                  Equations
                  Instances For
                    theorem WeierstrassCurve.Projective.polynomialZ_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) :
                    W.polynomialZ = MvPolynomial.X 1 ^ 2 + MvPolynomial.C W.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.C (2 * W.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 - (MvPolynomial.C W.a₂ * MvPolynomial.X 0 ^ 2 + MvPolynomial.C (2 * W.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C (3 * W.a₆) * MvPolynomial.X 2 ^ 2)
                    theorem WeierstrassCurve.Projective.eval_polynomialZ {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
                    (MvPolynomial.eval P) W.polynomialZ = P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 - (W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
                    theorem WeierstrassCurve.Projective.polynomial_relation {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
                    3 * (MvPolynomial.eval P) W.polynomial = P 0 * (MvPolynomial.eval P) W.polynomialX + P 1 * (MvPolynomial.eval P) W.polynomialY + P 2 * (MvPolynomial.eval P) W.polynomialZ

                    Euler's homogeneous function theorem.

                    The proposition that a point representative $(x, y, z)$ in W is nonsingular. In other words, either $W_X(x, y, z) \ne 0$, $W_Y(x, y, z) \ne 0$, or $W_Z(x, y, z) \ne 0$.

                    Equations
                    Instances For
                      theorem WeierstrassCurve.Projective.nonsingular_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
                      W.Nonsingular P W.Equation P (W.a₁ * P 1 * P 2 3 * P 0 ^ 2 + 2 * W.a₂ * P 0 * P 2 + W.a₄ * P 2 ^ 2 P 1 * P 2 -P 1 * P 2 - W.a₁ * P 0 * P 2 - W.a₃ * P 2 ^ 2 P 1 ^ 2 + W.a₁ * P 0 * P 1 + 2 * W.a₃ * P 1 * P 2 W.a₂ * P 0 ^ 2 + 2 * W.a₄ * P 0 * P 2 + 3 * W.a₆ * P 2 ^ 2)
                      theorem WeierstrassCurve.Projective.nonsingular_zero' {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) [NoZeroDivisors R] {Y : R} (hy : Y 0) :
                      W.Nonsingular ![0, Y, 0]
                      theorem WeierstrassCurve.Projective.nonsingular_some {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (X : R) (Y : R) :
                      W.Nonsingular ![X, Y, 1] W.toAffine.Nonsingular X Y
                      theorem WeierstrassCurve.Projective.nonsingular_smul_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) (u : Rˣ) :
                      W.Nonsingular (u P) W.Nonsingular P
                      theorem WeierstrassCurve.Projective.nonsingular_of_equiv {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) {P : Fin 3R} {Q : Fin 3R} (h : P Q) :
                      W.Nonsingular P W.Nonsingular Q

                      The proposition that a point class on W is nonsingular. If P is a point representative, then W.NonsingularLift ⟦P⟧ is definitionally equivalent to W.Nonsingular P.

                      Equations
                      Instances For
                        @[simp]
                        theorem WeierstrassCurve.Projective.nonsingularLift_iff {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (P : Fin 3R) :
                        W.NonsingularLift P W.Nonsingular P
                        theorem WeierstrassCurve.Projective.nonsingularLift_zero {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) [Nontrivial R] :
                        W.NonsingularLift ![0, 1, 0]
                        theorem WeierstrassCurve.Projective.nonsingularLift_zero' {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) [NoZeroDivisors R] {Y : R} (hy : Y 0) :
                        W.NonsingularLift ![0, Y, 0]
                        theorem WeierstrassCurve.Projective.nonsingularLift_some {R : Type u} [CommRing R] (W : WeierstrassCurve.Projective R) (X : R) (Y : R) :
                        W.NonsingularLift ![X, Y, 1] W.toAffine.Nonsingular X Y
                        theorem WeierstrassCurve.Projective.equiv_of_Z_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} {Q : Fin 3F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) :
                        P Q
                        theorem WeierstrassCurve.Projective.equiv_zero_of_Z_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (h : W.Nonsingular P) (hPz : P 2 = 0) :
                        P ![0, 1, 0]
                        theorem WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero {F : Type u} [Field F] {P : Fin 3F} (hPz : P 2 0) :
                        P ![P 0 / P 2, P 1 / P 2, 1]
                        theorem WeierstrassCurve.Projective.nonsingular_iff_affine_of_Z_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (hPz : P 2 0) :
                        W.Nonsingular P W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)
                        theorem WeierstrassCurve.Projective.nonsingular_of_affine_of_Z_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (h : W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)) (hPz : P 2 0) :
                        W.Nonsingular P
                        theorem WeierstrassCurve.Projective.nonsingular_affine_of_Z_ne_zero {F : Type u} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3F} (h : W.Nonsingular P) (hPz : P 2 0) :
                        W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)