The group law on point representatives of a projective Weierstrass curve

For a Weierstrass curve W' over a commutative ring, Mathlib's addition WeierstrassCurve.Projective.add of two point representatives P and Q is the doubling formula dblXYZ P if P and Q are equivalent, and the addition formula addXYZ P Q otherwise. Mathlib shows that over a field it induces a commutative group law on the nonsingular point classes. This file states laws of that group for point representatives, where they hold up to equivalence.

Commutativity holds over any commutative ring and for all point representatives: add P Q and add Q P are equivalent, because each coordinate of addXYZ changes sign when P and Q are swapped. Associativity and the inverse law are those of Mathlib's group, for nonsingular point representatives over a field. Over a field, the group law also commutes with a change of variables C: the homogeneous coordinate map P ↦ C.toMatrix *ᵥ P from C • W to W carries add P Q, for nonsingular point representatives P and Q of C • W, to a representative of add (C.toMatrix *ᵥ P) (C.toMatrix *ᵥ Q). This is read off the affine point groups, where the change of variables is the group isomorphism WeierstrassCurve.Affine.Point.addEquivVariableChange. Transported through the projective-affine comparison, that isomorphism is a group isomorphism of projective points given by the matrix C.toMatrix on homogeneous coordinates.

Main results

• WeierstrassCurve.Projective.addXYZ_swap: swapping the two point representatives changes the sign of the addition formula, addXYZ P Q = -addXYZ Q P.
• WeierstrassCurve.Projective.add_comm_equiv: the sums add P Q and add Q P of two point representatives are equivalent.
• WeierstrassCurve.Projective.add_assoc_equiv: over a field, the sums add (add P Q) T and add P (add Q T) of three nonsingular point representatives are equivalent.
• WeierstrassCurve.Projective.add_neg_equiv: over a field, the sum add P (neg P) of a nonsingular point representative and its negation is equivalent to ![0, 1, 0].
• WeierstrassCurve.Projective.Point.toAffine_eq_toAffine_iff: over a field, two nonsingular point representatives have the same affine point exactly when they are equivalent.
• WeierstrassCurve.Projective.Point.toAffine_toMatrix_mulVec: over a field, the affine point of C.toMatrix *ᵥ P is the image of the affine point of P under the change of variables C.
• WeierstrassCurve.Projective.toMatrix_mulVec_add_equiv: over a field, for nonsingular point representatives P and Q of C • W, the image of add P Q under C.toMatrix is equivalent to the sum add (C.toMatrix *ᵥ P) (C.toMatrix *ᵥ Q) on W.
• WeierstrassCurve.Projective.Point.addEquivVariableChange: over a field, the change of variables C as a group isomorphism from the projective points of C • W to those of W, given on homogeneous coordinates by C.toMatrix (Point.addEquivVariableChange_mk).

theorem WeierstrassCurve.Projective.addX_swap {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.addX P Q = -W'.addX Q P

Swapping the two point representatives changes the sign of the X-coordinate addX of the addition formula.

theorem WeierstrassCurve.Projective.addZ_swap {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.addZ P Q = -W'.addZ Q P

Swapping the two point representatives changes the sign of the Z-coordinate addZ of the addition formula.

theorem WeierstrassCurve.Projective.negAddY_swap {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.negAddY P Q = -W'.negAddY Q P

Swapping the two point representatives changes the sign of the negated Y-coordinate negAddY of the addition formula.

theorem WeierstrassCurve.Projective.addY_swap {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.addY P Q = -W'.addY Q P

Swapping the two point representatives changes the sign of the Y-coordinate addY of the addition formula.

theorem WeierstrassCurve.Projective.addXYZ_swap {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.addXYZ P Q = -W'.addXYZ Q P

Swapping the two point representatives changes the sign of the addition formula addXYZ.

theorem WeierstrassCurve.Projective.add_comm_equiv {R : Type u_1} [CommRing R] {W' : Projective R} (P Q : Fin 3 → R) : W'.add P Q ≈ W'.add Q P

The sums W'.add P Q and W'.add Q P of two point representatives on a Weierstrass curve over a commutative ring are equivalent.

theorem WeierstrassCurve.Projective.add_assoc_equiv {F : Type u_2} [Field F] {W : Projective F} {P Q T : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hT : W.Nonsingular T) : W.add (W.add P Q) T ≈ W.add P (W.add Q T)

Over a field, the sums W.add (W.add P Q) T and W.add P (W.add Q T) of three nonsingular point representatives are equivalent.

theorem WeierstrassCurve.Projective.add_neg_equiv {F : Type u_2} [Field F] {W : Projective F} {P : Fin 3 → F} (hP : W.Nonsingular P) : W.add P (W.neg P) ≈ ![0, 1, 0]

Over a field, the sum W.add P (W.neg P) of a nonsingular point representative and its negation is equivalent to the representative ![0, 1, 0] of the point at infinity.

theorem WeierstrassCurve.Projective.Point.toAffine_eq_toAffine_iff {F : Type u_2} [Field F] {W : Projective F} {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) : toAffine W P = toAffine W Q ↔ P ≈ Q

Over a field, two nonsingular point representatives have the same affine point exactly when they are equivalent.

@[simp]

theorem WeierstrassCurve.Projective.Point.toAffine_toMatrix_mulVec {F : Type u_2} [Field F] {W : WeierstrassCurve F} (C : VariableChange F) (P : Fin 3 → F) : toAffine W.toProjective (C.toMatrix.mulVec P) = (Affine.Point.equivVariableChange W C) (toAffine (C • W).toProjective P)

Over a field, the affine point of the image C.toMatrix *ᵥ P on W of a point representative P of C • W is the image of the affine point of P under the change of variables (x, y) ↦ (u²x + r, u³y + u²sx + t). Both sides are 0 when P is singular.

theorem WeierstrassCurve.Projective.toMatrix_mulVec_add_equiv {F : Type u_2} [Field F] {W : WeierstrassCurve F} (C : VariableChange F) {P Q : Fin 3 → F} (hP : (C • W).toProjective.Nonsingular P) (hQ : (C • W).toProjective.Nonsingular Q) : C.toMatrix.mulVec ((C • W).toProjective.add P Q) ≈ W.toProjective.add (C.toMatrix.mulVec P) (C.toMatrix.mulVec Q)

The group law commutes with a change of variables. Over a field, let P and Q be nonsingular point representatives of C • W. The image under C.toMatrix of their sum add P Q on C • W is equivalent to the sum add (C.toMatrix *ᵥ P) (C.toMatrix *ᵥ Q) of their images on W.

noncomputable def WeierstrassCurve.Projective.Point.addEquivVariableChange {F : Type u_2} [Field F] (W : WeierstrassCurve F) (C : VariableChange F) : (C • W).toProjective.Point ≃+ W.toProjective.Point

Over a field, the change of variables C as a group isomorphism from the projective points of C • W to those of W. On homogeneous coordinates it is [X : Y : Z] ↦ [u²X + rZ : u²sX + u³Y + tZ : Z], the matrix C.toMatrix (Point.addEquivVariableChange_mk).

@[simp]

theorem WeierstrassCurve.Projective.Point.addEquivVariableChange_mk {F : Type u_2} [Field F] {W : WeierstrassCurve F} (C : VariableChange F) {P : Fin 3 → F} (hP : (C • W).toProjective.NonsingularLift ⟦P⟧) : (addEquivVariableChange W C) { point := ⟦P⟧, nonsingular := hP } = { point := ⟦C.toMatrix.mulVec P⟧, nonsingular := ⋯ }

The change of variables C sends the point with homogeneous coordinates P to the point with homogeneous coordinates C.toMatrix *ᵥ P.

@[simp]

theorem WeierstrassCurve.Projective.Point.addEquivVariableChange_symm_mk {F : Type u_2} [Field F] {W : WeierstrassCurve F} (C : VariableChange F) {P : Fin 3 → F} (hP : W.toProjective.NonsingularLift ⟦P⟧) : (addEquivVariableChange W C).symm { point := ⟦P⟧, nonsingular := hP } = { point := ⟦C⁻¹.toMatrix.mulVec P⟧, nonsingular := ⋯ }

The inverse of the change of variables C sends the point with homogeneous coordinates P to the point with homogeneous coordinates C⁻¹.toMatrix *ᵥ P.