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

• WeierstrassCurve.Projective.PointClass: the equivalence class of a point representative.
• WeierstrassCurve.Projective.toAffine: the Weierstrass curve in affine coordinates.
• WeierstrassCurve.Projective.Nonsingular: the nonsingular condition on a point representative.
• WeierstrassCurve.Projective.NonsingularLift: the nonsingular condition on a point class.

Main statements

• WeierstrassCurve.Projective.polynomial_relation: Euler's homogeneous function theorem.

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 lemmas fin3_def and fin3_def_ext 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 Rˣ, or equivalently that there is some unit u of R such that P = u • Q. However, u • Q is not definitionally equal to ![u * Q x, u * Q y, u * Q z], so the 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) : Type u

An abbreviation for a Weierstrass curve in projective coordinates.

Equations

• WeierstrassCurve.Projective R = WeierstrassCurve R

@[reducible, inline]

abbrev WeierstrassCurve.toProjective {R : Type u} (W : WeierstrassCurve R) : WeierstrassCurve.Projective R

The coercion to a Weierstrass curve in projective coordinates.

Equations

• W.toProjective = W

Projective coordinates

theorem WeierstrassCurve.Projective.fin3_def {R : Type u} (P : Fin 3 → R) : ![P 0, P 1, P 2] = P

theorem WeierstrassCurve.Projective.fin3_def_ext {R : Type u} (X : R) (Y : R) (Z : R) : ![X, Y, Z] 0 = X ∧ ![X, Y, Z] 1 = Y ∧ ![X, Y, Z] 2 = Z

theorem WeierstrassCurve.Projective.comp_fin3 {R : Type u} {S : Type u_1} (f : R → S) (X : R) (Y : R) (Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z]

theorem WeierstrassCurve.Projective.smul_fin3 {R : Type u} [CommRing R] (P : Fin 3 → R) (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 3 → R) (u : R) : (u • P) 0 = u * P 0 ∧ (u • P) 1 = u * P 1 ∧ (u • P) 2 = u * P 2

def WeierstrassCurve.Projective.instSetoidPoint {R : Type u} [CommRing R] : Setoid (Fin 3 → R)

The equivalence setoid for a point representative.

Equations

• WeierstrassCurve.Projective.instSetoidPoint = MulAction.orbitRel Rˣ (Fin 3 → R)

@[reducible, inline]

abbrev WeierstrassCurve.Projective.PointClass (R : Type u) [CommRing R] : Type u

The equivalence class of a point representative.

Equations

• WeierstrassCurve.Projective.PointClass R = MulAction.orbitRel.Quotient Rˣ (Fin 3 → R)

theorem WeierstrassCurve.Projective.smul_equiv {R : Type u} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : u • P ≈ P

@[simp]

theorem WeierstrassCurve.Projective.smul_eq {R : Type u} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : ⟦u • P⟧ = ⟦P⟧

@[reducible, inline]

abbrev WeierstrassCurve.Projective.toAffine {R : Type u} (W' : WeierstrassCurve.Projective R) : WeierstrassCurve.Affine R

The coercion to a Weierstrass curve in affine coordinates.

Equations

• W'.toAffine = W'

theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq' {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (hz : P 2 = Q 2) (mem : Q 2 ∈ nonZeroDivisors R) : P ≈ Q ↔ P = Q

theorem WeierstrassCurve.Projective.equiv_iff_eq_of_Z_eq {R : Type u} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} {Q : Fin 3 → R} (hz : P 2 = Q 2) (hQz : Q 2 ≠ 0) : P ≈ Q ↔ P = Q

theorem WeierstrassCurve.Projective.Z_eq_zero_of_equiv {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (h : P ≈ Q) : P 2 = 0 ↔ Q 2 = 0

theorem WeierstrassCurve.Projective.X_eq_of_equiv {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (h : P ≈ Q) : P 0 * Q 2 = Q 0 * P 2

theorem WeierstrassCurve.Projective.Y_eq_of_equiv {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (h : P ≈ Q) : P 1 * Q 2 = Q 1 * P 2

theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_left {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (hPz : P 2 = 0) (hQz : Q 2 ≠ 0) : ¬P ≈ Q

theorem WeierstrassCurve.Projective.not_equiv_of_Z_eq_zero_right {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (hPz : P 2 ≠ 0) (hQz : Q 2 = 0) : ¬P ≈ Q

theorem WeierstrassCurve.Projective.not_equiv_of_X_ne {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (hx : P 0 * Q 2 ≠ Q 0 * P 2) : ¬P ≈ Q

theorem WeierstrassCurve.Projective.not_equiv_of_Y_ne {R : Type u} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (hy : P 1 * Q 2 ≠ Q 1 * P 2) : ¬P ≈ Q

theorem WeierstrassCurve.Projective.equiv_of_X_eq_of_Y_eq {F : Type v} [Field F] {P : Fin 3 → F} {Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) (hx : P 0 * Q 2 = Q 0 * P 2) (hy : P 1 * Q 2 = Q 1 * P 2) : P ≈ Q

theorem WeierstrassCurve.Projective.equiv_some_of_Z_ne_zero {F : Type v} [Field F] {P : Fin 3 → F} (hPz : P 2 ≠ 0) : P ≈ ![P 0 / P 2, P 1 / P 2, 1]

theorem WeierstrassCurve.Projective.X_eq_iff {F : Type v} [Field F] {P : Fin 3 → F} {Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : P 0 * Q 2 = Q 0 * P 2 ↔ P 0 / P 2 = Q 0 / Q 2

theorem WeierstrassCurve.Projective.Y_eq_iff {F : Type v} [Field F] {P : Fin 3 → F} {Q : Fin 3 → F} (hPz : P 2 ≠ 0) (hQz : Q 2 ≠ 0) : P 1 * Q 2 = Q 1 * P 2 ↔ P 1 / P 2 = Q 1 / Q 2

Weierstrass equations

noncomputable def WeierstrassCurve.Projective.polynomial {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] : MvPolynomial (Fin 3) R

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.

theorem WeierstrassCurve.Projective.eval_polynomial {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : (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)

theorem WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : (MvPolynomial.eval P) W.polynomial / P 2 ^ 3 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomial

def WeierstrassCurve.Projective.Equation {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3 → R) : Prop

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

Equations

• W'.Equation P = ((MvPolynomial.eval P) W'.polynomial = 0)

theorem WeierstrassCurve.Projective.equation_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : 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) = 0

theorem WeierstrassCurve.Projective.equation_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Equation (u • P) ↔ W'.Equation P

theorem WeierstrassCurve.Projective.equation_of_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (h : P ≈ Q) : W'.Equation P ↔ W'.Equation Q

theorem WeierstrassCurve.Projective.equation_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.Equation P ↔ P 0 ^ 3 = 0

theorem WeierstrassCurve.Projective.equation_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] : W'.Equation ![0, 1, 0]

theorem WeierstrassCurve.Projective.equation_some {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) : W'.Equation ![X, Y, 1] ↔ W'.toAffine.Equation X Y

theorem WeierstrassCurve.Projective.equation_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Equation P ↔ W.toAffine.Equation (P 0 / P 2) (P 1 / P 2)

theorem WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P 2 = 0) : P 0 = 0

Nonsingular Weierstrass equations

noncomputable def WeierstrassCurve.Projective.polynomialX {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] : MvPolynomial (Fin 3) R

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

Equations

• W'.polynomialX = (MvPolynomial.pderiv 0) W'.polynomial

theorem WeierstrassCurve.Projective.polynomialX_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing 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} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : (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)

theorem WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : (MvPolynomial.eval P) W.polynomialX / P 2 ^ 2 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomialX

noncomputable def WeierstrassCurve.Projective.polynomialY {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] : MvPolynomial (Fin 3) R

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

Equations

• W'.polynomialY = (MvPolynomial.pderiv 1) W'.polynomial

theorem WeierstrassCurve.Projective.polynomialY_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing 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} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : (MvPolynomial.eval P) W'.polynomialY = 2 * P 1 * P 2 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 2

theorem WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : (MvPolynomial.eval P) W.polynomialY / P 2 ^ 2 = Polynomial.evalEval (P 0 / P 2) (P 1 / P 2) W.toAffine.polynomialY

noncomputable def WeierstrassCurve.Projective.polynomialZ {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] : MvPolynomial (Fin 3) R

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

Equations

• W'.polynomialZ = (MvPolynomial.pderiv 2) W'.polynomial

theorem WeierstrassCurve.Projective.polynomialZ_eq {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing 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} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : (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} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : 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.

def WeierstrassCurve.Projective.Nonsingular {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : Fin 3 → R) : Prop

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$.

Note that this definition is only mathematically accurate for fields.

Equations

• W'.Nonsingular P = (W'.Equation P ∧ ((MvPolynomial.eval P) W'.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W'.polynomialY ≠ 0 ∨ (MvPolynomial.eval P) W'.polynomialZ ≠ 0))

theorem WeierstrassCurve.Projective.nonsingular_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : 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) ≠ 0 ∨ 2 * P 1 * P 2 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 2 ≠ 0 ∨ 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) ≠ 0)

theorem WeierstrassCurve.Projective.nonsingular_smul {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Nonsingular (u • P) ↔ W'.Nonsingular P

theorem WeierstrassCurve.Projective.nonsingular_of_equiv {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} {Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q

theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] {P : Fin 3 → R} (hPz : P 2 = 0) : W'.Nonsingular P ↔ W'.Equation P ∧ (3 * P 0 ^ 2 ≠ 0 ∨ P 1 ^ 2 + W'.a₁ * P 0 * P 1 - W'.a₂ * P 0 ^ 2 ≠ 0)

theorem WeierstrassCurve.Projective.nonsingular_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] : W'.Nonsingular ![0, 1, 0]

theorem WeierstrassCurve.Projective.nonsingular_some {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) : W'.Nonsingular ![X, Y, 1] ↔ W'.toAffine.Nonsingular X Y

theorem WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.Equation P ∧ ((MvPolynomial.eval P) W.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialY ≠ 0)

theorem WeierstrassCurve.Projective.Y_ne_zero_of_Z_eq_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P) (hPz : P 2 = 0) : P 1 ≠ 0

theorem WeierstrassCurve.Projective.isUnit_Y_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : IsUnit (P 1)

theorem WeierstrassCurve.Projective.equiv_of_Z_eq_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} {Q : Fin 3 → F} (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 v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : P ≈ ![0, 1, 0]

def WeierstrassCurve.Projective.NonsingularLift {R : Type u} (W' : WeierstrassCurve.Projective R) [CommRing R] (P : WeierstrassCurve.Projective.PointClass R) : Prop

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

• W'.NonsingularLift P = Quotient.lift W'.Nonsingular ⋯ P

theorem WeierstrassCurve.Projective.nonsingularLift_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) : W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P

theorem WeierstrassCurve.Projective.nonsingularLift_zero {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] : W'.NonsingularLift ⟦![0, 1, 0]⟧

theorem WeierstrassCurve.Projective.nonsingularLift_some {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (X : R) (Y : R) : W'.NonsingularLift ⟦![X, Y, 1]⟧ ↔ W'.toAffine.Nonsingular X Y

@[deprecated WeierstrassCurve.Projective.equation_smul]

theorem WeierstrassCurve.Projective.equation_smul_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Equation (u • P) ↔ W'.Equation P

Alias of WeierstrassCurve.Projective.equation_smul.

@[deprecated WeierstrassCurve.Projective.nonsingularLift_zero]

theorem WeierstrassCurve.Projective.nonsingularLift_zero' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] : W'.NonsingularLift ⟦![0, 1, 0]⟧

Alias of WeierstrassCurve.Projective.nonsingularLift_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]

theorem WeierstrassCurve.Projective.nonsingular_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]

theorem WeierstrassCurve.Projective.nonsingular_iff_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero]

theorem WeierstrassCurve.Projective.nonsingular_of_affine_of_Z_ne_zero {F : Type v} [Field F] {W : WeierstrassCurve.Projective F} {P : Fin 3 → F} (hPz : P 2 ≠ 0) : W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2) (P 1 / P 2)

Alias of WeierstrassCurve.Projective.nonsingular_of_Z_ne_zero.

@[deprecated WeierstrassCurve.Projective.nonsingular_smul]

theorem WeierstrassCurve.Projective.nonsingular_smul_iff {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] (P : Fin 3 → R) {u : R} (hu : IsUnit u) : W'.Nonsingular (u • P) ↔ W'.Nonsingular P

Alias of WeierstrassCurve.Projective.nonsingular_smul.

@[deprecated WeierstrassCurve.Projective.nonsingular_zero]

theorem WeierstrassCurve.Projective.nonsingular_zero' {R : Type u} {W' : WeierstrassCurve.Projective R} [CommRing R] [Nontrivial R] : W'.Nonsingular ![0, 1, 0]

Alias of WeierstrassCurve.Projective.nonsingular_zero.