Weierstrass equations and the nonsingular condition in Jacobian coordinates

A point on the projective plane over a commutative ring R with weights (2, 3, 1) is an equivalence class [x : y : z] of triples (x, y, z) ≠ (0, 0, 0) of elements in R such that (x, y, z) ∼ (x', y', z') if there is some unit u in Rˣ with (x, y, z) = (u²x', u³y', uz').

Let W be a Weierstrass curve over a commutative ring R with coefficients aᵢ. A Jacobian point is a point on the projective plane over R with weights (2, 3, 1) satisfying the (2, 3, 1)-homogeneous Weierstrass equation W(X, Y, Z) = 0 in Jacobian coordinates, where W(X, Y, Z) := Y² + a₁XYZ + a₃YZ³ - (X³ + a₂X²Z² + a₄XZ⁴ + a₆Z⁶). It is nonsingular if its partial derivatives W_X(x, y, z), W_Y(x, y, z), and W_Z(x, y, z) do not vanish simultaneously.

This file gives an explicit implementation of equivalence classes of triples up to scaling by weights, and defines polynomials associated to Weierstrass equations and the nonsingular condition in Jacobian coordinates. The group law on the actual type of nonsingular Jacobian points will be defined in Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Point.lean, based on the formulae for group operations in Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Formula.lean.

Main definitions

• WeierstrassCurve.Jacobian.PointClass: the equivalence class of a point representative.
• WeierstrassCurve.Jacobian.Nonsingular: the nonsingular condition on a point representative.
• WeierstrassCurve.Jacobian.NonsingularLift: the nonsingular condition on a point class.

Main statements

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

Implementation notes

All definitions and lemmas for Weierstrass curves in Jacobian coordinates live in the namespace WeierstrassCurve.Jacobian to distinguish them from those in other coordinates. This is simply an abbreviation for WeierstrassCurve that can be converted using WeierstrassCurve.toJacobian. This can be converted into WeierstrassCurve.Affine using WeierstrassCurve.Jacobian.toAffine.

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 syntactically 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 syntactically 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. Files in Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian make extensive use of erw to get around this. While erw is often an indication of a problem, in this case it is self-contained and should not cause any issues. It would alternatively be possible to add some automation to assist here.

Whenever possible, all changes to documentation and naming of definitions and theorems should be mirrored in Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean.

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, Jacobian, Weierstrass equation, nonsingular

Jacobian coordinates

@[reducible, inline]

abbrev WeierstrassCurve.Jacobian (R : Type r) : Type r

An abbreviation for a Weierstrass curve in Jacobian coordinates.

Equations

• WeierstrassCurve.Jacobian R = WeierstrassCurve R

@[reducible, inline]

abbrev WeierstrassCurve.toJacobian {R : Type r} (W : WeierstrassCurve R) : Jacobian R

The conversion from a Weierstrass curve to Jacobian coordinates.

Equations

• W.toJacobian = W

@[reducible, inline]

abbrev WeierstrassCurve.Jacobian.toAffine {R : Type r} (W' : Affine R) : Affine R

The conversion from a Weierstrass curve in Jacobian coordinates to affine coordinates.

Equations

• WeierstrassCurve.Jacobian.toAffine W' = W'

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

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

theorem WeierstrassCurve.Jacobian.comp_fin3 {R : Type r} {S : Type s} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z]

def WeierstrassCurve.Jacobian.instSMulForallFinOfNatNat {R : Type r} [CommRing R] : SMul R (Fin 3 → R)

The scalar multiplication for a Jacobian point representative on a Weierstrass curve.

Equations

• WeierstrassCurve.Jacobian.instSMulForallFinOfNatNat = { smul := fun (u : R) (P : Fin 3 → R) => ![u ^ 2 * P 0, u ^ 3 * P 1, u * P 2] }

theorem WeierstrassCurve.Jacobian.smul_fin3 {R : Type r} [CommRing R] (P : Fin 3 → R) (u : R) : u • P = ![u ^ 2 * P 0, u ^ 3 * P 1, u * P 2]

theorem WeierstrassCurve.Jacobian.smul_fin3_ext {R : Type r} [CommRing R] (P : Fin 3 → R) (u : R) : (u • P) 0 = u ^ 2 * P 0 ∧ (u • P) 1 = u ^ 3 * P 1 ∧ (u • P) 2 = u * P 2

theorem WeierstrassCurve.Jacobian.comp_smul {R : Type r} {S : Type s} [CommRing R] [CommRing S] (f : R →+* S) (P : Fin 3 → R) (u : R) : ⇑f ∘ (u • P) = f u • ⇑f ∘ P

@[deprecated WeierstrassCurve.Jacobian.comp_smul (since := "2025-01-30")]

theorem WeierstrassCurve.Jacobian.map_smul {R : Type r} {S : Type s} [CommRing R] [CommRing S] (f : R →+* S) (P : Fin 3 → R) (u : R) : ⇑f ∘ (u • P) = f u • ⇑f ∘ P

Alias of WeierstrassCurve.Jacobian.comp_smul.

def WeierstrassCurve.Jacobian.instMulActionForallFinOfNatNat {R : Type r} [CommRing R] : MulAction R (Fin 3 → R)

The multiplicative action for a Jacobian point representative on a Weierstrass curve.

Equations

• WeierstrassCurve.Jacobian.instMulActionForallFinOfNatNat = MulAction.mk ⋯ ⋯

@[reducible]

def WeierstrassCurve.Jacobian.instSetoidForallFinOfNatNat {R : Type r} [CommRing R] : Setoid (Fin 3 → R)

The equivalence setoid for a Jacobian point representative on a Weierstrass curve.

Equations

• WeierstrassCurve.Jacobian.instSetoidForallFinOfNatNat = MulAction.orbitRel Rˣ (Fin 3 → R)

@[reducible, inline]

abbrev WeierstrassCurve.Jacobian.PointClass (R : Type r) [CommRing R] : Type r

The equivalence class of a Jacobian point representative on a Weierstrass curve.

Equations

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

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

@[simp]

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

theorem WeierstrassCurve.Jacobian.smul_equiv_smul {R : Type r} [CommRing R] (P Q : Fin 3 → R) {u v : R} (hu : IsUnit u) (hv : IsUnit v) : u • P ≈ v • Q ↔ P ≈ Q

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

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

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

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

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

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

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

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

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

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

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

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

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

Weierstrass equations in Jacobian coordinates

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

The polynomial W(X, Y, Z) := Y² + a₁XYZ + a₃YZ³ - (X³ + a₂X²Z² + a₄XZ⁴ + a₆Z⁶) associated to a Weierstrass curve W over a ring R in Jacobian coordinates.

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.Jacobian.eval_polynomial {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : (MvPolynomial.eval P) W'.polynomial = P 1 ^ 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 3 - (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 ^ 2 + W'.a₄ * P 0 * P 2 ^ 4 + W'.a₆ * P 2 ^ 6)

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

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

The proposition that a Jacobian point representative (x, y, z) lies in a Weierstrass curve W.

In other words, it satisfies the (2, 3, 1)-homogeneous Weierstrass equation W(X, Y, Z) = 0.

Equations

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

theorem WeierstrassCurve.Jacobian.equation_iff {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : W'.Equation P ↔ P 1 ^ 2 + W'.a₁ * P 0 * P 1 * P 2 + W'.a₃ * P 1 * P 2 ^ 3 - (P 0 ^ 3 + W'.a₂ * P 0 ^ 2 * P 2 ^ 2 + W'.a₄ * P 0 * P 2 ^ 4 + W'.a₆ * P 2 ^ 6) = 0

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

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

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

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

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

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

The nonsingular condition in Jacobian coordinates

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

The partial derivative W_X(X, Y, Z) with respect to X of the polynomial W(X, Y, Z) associated to a Weierstrass curve W in Jacobian coordinates.

Equations

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

theorem WeierstrassCurve.Jacobian.polynomialX_eq {R : Type r} [CommRing R] {W' : Jacobian 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 ^ 2 + MvPolynomial.C W'.a₄ * MvPolynomial.X 2 ^ 4)

theorem WeierstrassCurve.Jacobian.eval_polynomialX {R : Type r} [CommRing R] {W' : Jacobian 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 ^ 2 + W'.a₄ * P 2 ^ 4)

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

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

The partial derivative W_Y(X, Y, Z) with respect to Y of the polynomial W(X, Y, Z) associated to a Weierstrass curve W in Jacobian coordinates.

Equations

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

theorem WeierstrassCurve.Jacobian.polynomialY_eq {R : Type r} [CommRing R] {W' : Jacobian R} : W'.polynomialY = MvPolynomial.C 2 * MvPolynomial.X 1 + MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 2 + MvPolynomial.C W'.a₃ * MvPolynomial.X 2 ^ 3

theorem WeierstrassCurve.Jacobian.eval_polynomialY {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : (MvPolynomial.eval P) W'.polynomialY = 2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3

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

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

The partial derivative W_Z(X, Y, Z) with respect to Z of the polynomial W(X, Y, Z) associated to a Weierstrass curve W in Jacobian coordinates.

Equations

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

theorem WeierstrassCurve.Jacobian.polynomialZ_eq {R : Type r} [CommRing R] {W' : Jacobian R} : W'.polynomialZ = MvPolynomial.C W'.a₁ * MvPolynomial.X 0 * MvPolynomial.X 1 + MvPolynomial.C (3 * W'.a₃) * MvPolynomial.X 1 * MvPolynomial.X 2 ^ 2 - (MvPolynomial.C (2 * W'.a₂) * MvPolynomial.X 0 ^ 2 * MvPolynomial.X 2 + MvPolynomial.C (4 * W'.a₄) * MvPolynomial.X 0 * MvPolynomial.X 2 ^ 3 + MvPolynomial.C (6 * W'.a₆) * MvPolynomial.X 2 ^ 5)

theorem WeierstrassCurve.Jacobian.eval_polynomialZ {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : (MvPolynomial.eval P) W'.polynomialZ = W'.a₁ * P 0 * P 1 + 3 * W'.a₃ * P 1 * P 2 ^ 2 - (2 * W'.a₂ * P 0 ^ 2 * P 2 + 4 * W'.a₄ * P 0 * P 2 ^ 3 + 6 * W'.a₆ * P 2 ^ 5)

theorem WeierstrassCurve.Jacobian.polynomial_relation {R : Type r} [CommRing R] {W' : Jacobian R} (P : Fin 3 → R) : 6 * (MvPolynomial.eval P) W'.polynomial = 2 * P 0 * (MvPolynomial.eval P) W'.polynomialX + 3 * P 1 * (MvPolynomial.eval P) W'.polynomialY + P 2 * (MvPolynomial.eval P) W'.polynomialZ

Euler's homogeneous function theorem in Jacobian coordinates.

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

The proposition that a Jacobian point representative (x, y, z) on a Weierstrass curve W is nonsingular.

In other words, either W_X(x, y, z) ≠ 0, W_Y(x, y, z) ≠ 0, or W_Z(x, y, z) ≠ 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.Jacobian.nonsingular_iff {R : Type r} [CommRing R] {W' : Jacobian 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 ^ 2 + W'.a₄ * P 2 ^ 4) ≠ 0 ∨ 2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3 ≠ 0 ∨ W'.a₁ * P 0 * P 1 + 3 * W'.a₃ * P 1 * P 2 ^ 2 - (2 * W'.a₂ * P 0 ^ 2 * P 2 + 4 * W'.a₄ * P 0 * P 2 ^ 3 + 6 * W'.a₆ * P 2 ^ 5) ≠ 0)

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

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

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

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

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

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

theorem WeierstrassCurve.Jacobian.nonsingular_iff_of_Z_ne_zero {F : Type u} [Field F] {W : Jacobian 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.Jacobian.X_ne_zero_of_Z_eq_zero {R : Type r} [CommRing R] {W' : Jacobian R} [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P) (hPz : P 2 = 0) : P 0 ≠ 0

theorem WeierstrassCurve.Jacobian.isUnit_X_of_Z_eq_zero {F : Type u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : IsUnit (P 0)

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

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

theorem WeierstrassCurve.Jacobian.equiv_of_Z_eq_zero {F : Type u} [Field F] {W : Jacobian F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P 2 = 0) (hQz : Q 2 = 0) : P ≈ Q

theorem WeierstrassCurve.Jacobian.equiv_zero_of_Z_eq_zero {F : Type u} [Field F] {W : Jacobian F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : P ≈ ![1, 1, 0]

theorem WeierstrassCurve.Jacobian.comp_equiv_comp {F : Type u} {K : Type v} [Field F] [Field K] {W : Jacobian F} (f : F →+* K) {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : ⇑f ∘ P ≈ ⇑f ∘ Q ↔ P ≈ Q

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

The proposition that a Jacobian point class on a Weierstrass curve W is nonsingular.

If P is a Jacobian point representative on W, then W.NonsingularLift ⟦P⟧ is definitionally equivalent to W.Nonsingular P.

Note that this definition is only mathematically accurate for fields.

Equations

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

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

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

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

Maps and base changes

@[simp]

theorem WeierstrassCurve.Jacobian.map_polynomial {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (f : R →+* S) : (map W' f).toJacobian.polynomial = (MvPolynomial.map f) W'.polynomial

theorem WeierstrassCurve.Jacobian.Equation.map {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (f : R →+* S) {P : Fin 3 → R} (h : W'.Equation P) : (WeierstrassCurve.map W' f).toJacobian.Equation (⇑f ∘ P)

@[simp]

theorem WeierstrassCurve.Jacobian.map_equation {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} {f : R →+* S} (P : Fin 3 → R) (hf : Function.Injective ⇑f) : (map W' f).toJacobian.Equation (⇑f ∘ P) ↔ W'.Equation P

@[simp]

theorem WeierstrassCurve.Jacobian.map_polynomialX {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (f : R →+* S) : (map W' f).toJacobian.polynomialX = (MvPolynomial.map f) W'.polynomialX

@[simp]

theorem WeierstrassCurve.Jacobian.map_polynomialY {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (f : R →+* S) : (map W' f).toJacobian.polynomialY = (MvPolynomial.map f) W'.polynomialY

@[simp]

theorem WeierstrassCurve.Jacobian.map_polynomialZ {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} (f : R →+* S) : (map W' f).toJacobian.polynomialZ = (MvPolynomial.map f) W'.polynomialZ

@[simp]

theorem WeierstrassCurve.Jacobian.map_nonsingular {R : Type r} {S : Type s} [CommRing R] [CommRing S] {W' : Jacobian R} {f : R →+* S} (P : Fin 3 → R) (hf : Function.Injective ⇑f) : (map W' f).toJacobian.Nonsingular (⇑f ∘ P) ↔ W'.Nonsingular P

theorem WeierstrassCurve.Jacobian.baseChange_polynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomial = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomial

theorem WeierstrassCurve.Jacobian.Equation.baseChange {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) {P : Fin 3 → A} (h : (WeierstrassCurve.baseChange W' A).toJacobian.Equation P) : (WeierstrassCurve.baseChange W' B).toJacobian.Equation (⇑f ∘ P)

theorem WeierstrassCurve.Jacobian.baseChange_equation {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {f : A →ₐ[S] B} (P : Fin 3 → A) (hf : Function.Injective ⇑f) : (baseChange W' B).toJacobian.Equation (⇑f ∘ P) ↔ (baseChange W' A).toJacobian.Equation P

theorem WeierstrassCurve.Jacobian.baseChange_polynomialX {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomialX = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialX

theorem WeierstrassCurve.Jacobian.baseChange_polynomialY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomialY = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialY

theorem WeierstrassCurve.Jacobian.baseChange_polynomialZ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) : (baseChange W' B).toJacobian.polynomialZ = (MvPolynomial.map ↑f) (baseChange W' A).toJacobian.polynomialZ

theorem WeierstrassCurve.Jacobian.baseChange_nonsingular {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Jacobian R} [Algebra R S] [Algebra R A] [Algebra S A] [IsScalarTower R S A] [Algebra R B] [Algebra S B] [IsScalarTower R S B] {f : A →ₐ[S] B} (P : Fin 3 → A) (hf : Function.Injective ⇑f) : (baseChange W' B).toJacobian.Nonsingular (⇑f ∘ P) ↔ (baseChange W' A).toJacobian.Nonsingular P