Weierstrass equations and the nonsingular condition in projective coordinates

A point on the unweighted projective plane over a commutative ring R 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) = (ux', uy', uz').

Let W be a Weierstrass curve over a commutative ring R with coefficients aᵢ. A projective point is a point on the unweighted projective plane over R satisfying the homogeneous Weierstrass equation W(X, Y, Z) = 0 in projective coordinates, where W(X, Y, Z) := Y²Z + 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 units, and defines polynomials associated to Weierstrass equations and the nonsingular condition in projective coordinates. The group law on the actual type of nonsingular projective points will be defined in Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Point.lean, based on the formulae for group operations in Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Formula.lean.

Main definitions

• WeierstrassCurve.Projective.PointClass: the equivalence class of a point representative.
• 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

All definitions and lemmas for Weierstrass curves in projective coordinates live in the namespace WeierstrassCurve.Projective to distinguish them from those in other coordinates. This is simply an abbreviation for WeierstrassCurve that can be converted using WeierstrassCurve.toProjective. This can be converted into WeierstrassCurve.Affine using WeierstrassCurve.Projective.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 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. Files in Mathlib/AlgebraicGeometry/EllipticCurve/Projective 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/Jacobian/Basic.lean.

References

J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, projective, Weierstrass equation, nonsingular

Projective coordinates

@[reducible, inline]

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

An abbreviation for a Weierstrass curve in projective coordinates.

Equations

• WeierstrassCurve.Projective R = WeierstrassCurve R

@[reducible, inline]

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

The conversion from a Weierstrass curve to projective coordinates.

Equations

• W.toProjective = W

@[reducible, inline]

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

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

Equations

• WeierstrassCurve.Projective.toAffine W' = W'

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

theorem WeierstrassCurve.Projective.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.Projective.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]

theorem WeierstrassCurve.Projective.smul_fin3 {R : Type r} [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 r} [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

theorem WeierstrassCurve.Projective.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

@[reducible]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

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

@[simp]

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

theorem WeierstrassCurve.Projective.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.Projective.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.Projective.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.Projective.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.Projective.X_eq_of_equiv {R : Type r} [CommRing R] {P Q : Fin 3 → R} (h : P ≈ Q) : P 0 * Q 2 = Q 0 * P 2

theorem WeierstrassCurve.Projective.Y_eq_of_equiv {R : Type r} [CommRing R] {P 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 r} [CommRing R] {P 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 r} [CommRing R] {P Q : Fin 3 → R} (hPz : P 2 ≠ 0) (hQz : Q 2 = 0) : ¬P ≈ Q

theorem WeierstrassCurve.Projective.not_equiv_of_X_ne {R : Type r} [CommRing R] {P 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 r} [CommRing R] {P 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 u} [Field F] {P 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 u} [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 u} [Field F] {P 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 u} [Field F] {P 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 in projective coordinates

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

The polynomial W(X, Y, Z) := Y²Z + a₁XYZ + a₃YZ² - (X³ + a₂X²Z + a₄XZ² + a₆Z³) associated to a Weierstrass curve W over a ring R in projective 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.Projective.eval_polynomial {R : Type r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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) (toAffine W).polynomial

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

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

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

Equations

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

theorem WeierstrassCurve.Projective.equation_iff {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Equation P ↔ W'.Equation Q

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

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

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

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

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

The nonsingular condition in projective coordinates

noncomputable def WeierstrassCurve.Projective.polynomialX {R : Type r} [CommRing R] (W' : Projective 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 projective coordinates.

Equations

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

theorem WeierstrassCurve.Projective.polynomialX_eq {R : Type r} [CommRing R] {W' : 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 r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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) (toAffine W).polynomialX

noncomputable def WeierstrassCurve.Projective.polynomialY {R : Type r} [CommRing R] (W' : Projective 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 projective coordinates.

Equations

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

theorem WeierstrassCurve.Projective.polynomialY_eq {R : Type r} [CommRing R] {W' : 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 r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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) (toAffine W).polynomialY

noncomputable def WeierstrassCurve.Projective.polynomialZ {R : Type r} [CommRing R] (W' : Projective 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 projective coordinates.

Equations

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

theorem WeierstrassCurve.Projective.polynomialZ_eq {R : Type r} [CommRing R] {W' : 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 r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 in projective coordinates.

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

The proposition that a projective 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.Projective.nonsingular_iff {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective R} {P Q : Fin 3 → R} (h : P ≈ Q) : W'.Nonsingular P ↔ W'.Nonsingular Q

theorem WeierstrassCurve.Projective.nonsingular_of_Z_eq_zero {R : Type r} [CommRing R] {W' : Projective 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 r} [CommRing R] {W' : Projective R} [Nontrivial R] : W'.Nonsingular ![0, 1, 0]

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

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

theorem WeierstrassCurve.Projective.nonsingular_iff_of_Z_ne_zero {F : Type u} [Field F] {W : 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 r} [CommRing R] {W' : Projective 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 u} [Field F] {W : 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 u} [Field F] {W : Projective 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.Projective.equiv_zero_of_Z_eq_zero {F : Type u} [Field F] {W : Projective F} {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P 2 = 0) : P ≈ ![0, 1, 0]

theorem WeierstrassCurve.Projective.comp_equiv_comp {F : Type u} {K : Type v} [Field F] [Field K] {W : Projective 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.Projective.NonsingularLift {R : Type r} [CommRing R] (W' : Projective R) (P : PointClass R) : Prop

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

If P is a projective 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.Projective.nonsingularLift_iff {R : Type r} [CommRing R] {W' : Projective R} (P : Fin 3 → R) : W'.NonsingularLift ⟦P⟧ ↔ W'.Nonsingular P

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

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

Maps and base changes

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem WeierstrassCurve.Projective.baseChange_polynomial {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.polynomial = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomial

theorem WeierstrassCurve.Projective.Equation.baseChange {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.Equation P) : (WeierstrassCurve.baseChange W' B).toProjective.Equation (⇑f ∘ P)

theorem WeierstrassCurve.Projective.baseChange_equation {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.Equation (⇑f ∘ P) ↔ (baseChange W' A).toProjective.Equation P

theorem WeierstrassCurve.Projective.baseChange_polynomialX {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.polynomialX = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomialX

theorem WeierstrassCurve.Projective.baseChange_polynomialY {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.polynomialY = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomialY

theorem WeierstrassCurve.Projective.baseChange_polynomialZ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.polynomialZ = (MvPolynomial.map ↑f) (baseChange W' A).toProjective.polynomialZ

theorem WeierstrassCurve.Projective.baseChange_nonsingular {R : Type r} {S : Type s} {A : Type u} {B : Type v} [CommRing R] [CommRing S] [CommRing A] [CommRing B] {W' : Projective 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).toProjective.Nonsingular (⇑f ∘ P) ↔ (baseChange W' A).toProjective.Nonsingular P