Unimodular solutions of the projective Weierstrass equation

For a Weierstrass curve W over a commutative ring R, a projective point class [X : Y : Z] is unimodular if it is represented by a solution of the projective Weierstrass equation whose coordinates are unimodular, that is, generate the unit ideal of R. Over a local ring these are exactly the solutions one of whose coordinates is a unit, and they describe the R-points of the projective Weierstrass model.

Mathlib's WeierstrassCurve.Projective.NonsingularLift is the corresponding condition with nonsingularity in place of unimodularity, and it is only meaningful over a field. Over a field and for an elliptic curve the two conditions agree, which identifies the unimodular classes with Mathlib's nonsingular projective points WeierstrassCurve.Projective.Point.

Main definitions

• WeierstrassCurve.Projective.UnimodularLift: the proposition that a projective point class is represented by a solution of the projective Weierstrass equation with unimodular coordinates.
• WeierstrassCurve.Projective.Point.equivUnimodularLift: on an elliptic curve over a field, the nonsingular projective points are the unimodular point classes.

Main results

• WeierstrassCurve.Projective.unimodularLift_iff: the condition on a representative.
• WeierstrassCurve.Projective.unimodularLift_iff_nonsingularLift: on an elliptic curve over a field, a point class is unimodular if and only if it is nonsingular.

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

The proposition that a projective point class on a Weierstrass curve W is represented by a solution of the projective Weierstrass equation with unimodular coordinates, that is, coordinates generating the unit ideal.

If P is a projective point representative on W, then W.UnimodularLift ⟦P⟧ is equivalent to W.Equation P ∧ Module.IsUnimodular R P (unimodularLift_iff). Over a local ring these classes correspond to the R-points of the projective Weierstrass model.

Equations

• W'.UnimodularLift P = Quotient.lift (fun (Q : Fin 3 → R) => W'.Equation Q ∧ Module.IsUnimodular R Q) ⋯ P

theorem WeierstrassCurve.Projective.unimodularLift_iff {R : Type u_1} [CommRing R] {W' : Projective R} (P : Fin 3 → R) : W'.UnimodularLift ⟦P⟧ ↔ W'.Equation P ∧ Module.IsUnimodular R P

The class of a representative P is unimodular if and only if P solves the projective Weierstrass equation and its coordinates are unimodular.

@[simp]

theorem WeierstrassCurve.Projective.unimodularLift_zero {R : Type u_1} [CommRing R] (W' : Projective R) : W'.UnimodularLift ⟦![0, 1, 0]⟧

The class of (0, 1, 0), the point at infinity [0 : 1 : 0], is unimodular.

@[simp]

theorem WeierstrassCurve.Projective.unimodularLift_some {R : Type u_1} [CommRing R] (W' : Projective R) (a b : R) : W'.UnimodularLift ⟦![a, b, 1]⟧ ↔ W'.toAffine.Equation a b

The class of (a, b, 1) is unimodular if and only if (a, b) solves the affine Weierstrass equation: the coordinate 1 makes the coordinates unimodular.

theorem WeierstrassCurve.Projective.unimodularLift_iff_nonsingularLift {F : Type u_1} [Field F] {W : Projective F} [WeierstrassCurve.IsElliptic W] {P : PointClass F} : W.UnimodularLift P ↔ W.NonsingularLift P

On an elliptic curve over a field, a projective point class is unimodular if and only if it is nonsingular: both conditions say that a nonzero representative solves the equation.

def WeierstrassCurve.Projective.Point.equivUnimodularLift {F : Type u_1} [Field F] (W : Projective F) [WeierstrassCurve.IsElliptic W] : W.Point ≃ { P : PointClass F // W.UnimodularLift P }

On an elliptic curve over a field, the nonsingular projective points are the unimodular projective point classes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem WeierstrassCurve.Projective.Point.coe_equivUnimodularLift {F : Type u_1} [Field F] (W : Projective F) [WeierstrassCurve.IsElliptic W] (P : W.Point) : ↑((equivUnimodularLift W) P) = P.point

@[simp]

theorem WeierstrassCurve.Projective.Point.equivUnimodularLift_symm_point {F : Type u_1} [Field F] (W : Projective F) [WeierstrassCurve.IsElliptic W] (P : { P : PointClass F // W.UnimodularLift P }) : ((equivUnimodularLift W).symm P).point = ↑P