feat(EllipticCurve): lemmas in Jacobian coordinates (#13846)

+ `equiv_iff_eq_of_Z_eq`: if a point has two representations in Jacobian coordinates with the same, nonzero Z-coordinate, then the two representations are equal.

+ `nonsingular_iff_of_Z_ne_zero`: a lemma deleted in an earlier PR for no reason, now restored.

+ `addXYZ_self`: if the addition (not doubling) formula is applied to a point representative and itself, the result is (0,0,0).

+ `addXYZ_neg`: the addition formula applied to a point representative and its negation yields a representative of the point at infinity.

+ two trivial lemmas `fromAffine_ne_zero` and `comp_fin3`.

+ a series of `map` lemmas showing the addition and doubling formulas in Jacobian coordinates commute with ring homomorphisms.



Co-authored-by: Junyan Xu <[email protected]>

Mathlib/Algebra/MvPolynomial/PDeriv.lean

@@ -127,6 +127,13 @@ theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a
 set_option linter.uppercaseLean3 false in
 #align mv_polynomial.pderiv_C_mul MvPolynomial.pderiv_C_mul
 
+theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :
+    pderiv i (map φ f) = map φ (pderiv i f) := by
+  apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_
+  obtain rfl | h := eq_or_ne j i
+  · simp [eq]
+  · simp [eq, h]
+
 end PDeriv
 
 end MvPolynomial

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean

@@ -6,6 +6,7 @@ Authors: David Kurniadi Angdinata
 import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.Algebra.MvPolynomial.PDeriv
 import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
+import Mathlib.Data.Fin.Tuple.Reflection
 
 /-!
 # Jacobian coordinates for Weierstrass curves
@@ -50,7 +51,7 @@ Note that most computational proofs follow from their analogous proofs for affin
  * `WeierstrassCurve.Jacobian.Point.neg`: the negation operation on a nonsingular rational point.
  * `WeierstrassCurve.Jacobian.Point.add`: the addition operation on a nonsingular rational point.
  * `WeierstrassCurve.Jacobian.Point.toAffineAddEquiv`: the equivalence between the nonsingular
-    rational points on a Jacobian Weierstrass curve with those on an affine Weierstrass curve.
+    rational points on a Weierstrass curve in Jacobian coordinates with those in affine coordinates.
 
 ## Main statements
 
@@ -63,9 +64,9 @@ A point representative is implemented as a term `P` of type `Fin 3 → R`, which
 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 ^ 2 * Q x, u ^ 3 * Q y, u * Q z]`,
-so the lemmas `smul_fin3` and `smul_fin3_ext` can be used to convert between the two forms.
+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.
 
 ## References
 
@@ -123,6 +124,9 @@ lemma fin3_def (P : Fin 3 → R) : ![P x, P y, P z] = P := by
 lemma fin3_def_ext (X Y Z : R) : ![X, Y, Z] x = X ∧ ![X, Y, Z] y = Y ∧ ![X, Y, Z] z = Z :=
   ⟨rfl, rfl, rfl⟩
 
+lemma comp_fin3 {S} (f : R → S) (X Y Z : R) : f ∘ ![X, Y, Z] = ![f X, f Y, f Z] :=
+  (FinVec.map_eq _ _).symm
+
 /-- The scalar multiplication on a point representative. -/
 scoped instance instSMulPoint : SMul R <| Fin 3 → R :=
   ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩
@@ -136,8 +140,8 @@ lemma smul_fin3_ext (P : Fin 3 → R) (u : R) :
 
 /-- The multiplicative action on a point representative. -/
 scoped instance instMulActionPoint : MulAction R <| Fin 3 → R where
-  one_smul _ := by simp only [smul_fin3, one_pow, one_mul, fin3_def]
-  mul_smul _ _ _ := by simp only [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]
+  one_smul _ := by simp_rw [smul_fin3, one_pow, one_mul, fin3_def]
+  mul_smul _ _ _ := by simp_rw [smul_fin3, mul_pow, mul_assoc, fin3_def_ext]
 
 /-- The equivalence setoid for a point representative. -/
 scoped instance instSetoidPoint : Setoid <| Fin 3 → R :=
@@ -160,6 +164,17 @@ variable (W') in
 abbrev toAffine : Affine R :=
   W'
 
+lemma equiv_iff_eq_of_Z_eq' {P Q : Fin 3 → R} (hz : P z = Q z) (mem : Q z ∈ nonZeroDivisors R) :
+    P ≈ Q ↔ P = Q := by
+  refine ⟨?_, by rintro rfl; exact Setoid.refl _⟩
+  rintro ⟨u, rfl⟩
+  rw [← one_mul (Q z)] at hz
+  simp_rw [Units.smul_def, (mul_cancel_right_mem_nonZeroDivisors mem).mp hz, one_smul]
+
+lemma equiv_iff_eq_of_Z_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hz : P z = Q z) (hQz : Q z ≠ 0) :
+    P ≈ Q ↔ P = Q :=
+  equiv_iff_eq_of_Z_eq' hz (mem_nonZeroDivisors_of_ne_zero hQz)
+
 lemma Z_eq_zero_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : P z = 0 ↔ Q z = 0 := by
   rcases h with ⟨_, rfl⟩
   simp only [Units.smul_def, smul_fin3_ext, Units.mul_right_eq_zero]
@@ -390,6 +405,12 @@ lemma nonsingular_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
     W.Nonsingular P ↔ W.toAffine.Nonsingular (P x / P z ^ 2) (P y / P z ^ 3) :=
   (nonsingular_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| nonsingular_some ..
 
+lemma nonsingular_iff_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :
+    W.Nonsingular P ↔ W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0) := by
+  rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
+    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 4 hPz,
+    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz]
+
 lemma X_ne_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsingular P)
     (hPz : P z = 0) : P x ≠ 0 := by
   intro hPx
@@ -521,6 +542,11 @@ lemma Y_eq_negY_of_Y_eq [NoZeroDivisors R] {P Q : Fin 3 → R} (hQz : Q z ≠ 0)
   mul_left_injective₀ (pow_ne_zero 3 hQz) <| by
     linear_combination (norm := ring1) -Y_sub_Y_add_Y_sub_negY P Q hx + hy + hy'
 
+lemma nonsingular_iff_of_Y_eq_negY {P : Fin 3 → F} (hPz : P z ≠ 0) (hy : P y = W.negY P) :
+    W.Nonsingular P ↔ W.Equation P ∧ eval P W.polynomialX ≠ 0 := by
+  rw [nonsingular_iff_of_Z_ne_zero hPz, show eval P W.polynomialY = P y - W.negY P by
+      rw [negY, eval_polynomialY]; ring1, hy, sub_self, ne_self_iff_false, or_false]
+
 end Negation
 
 section Doubling
@@ -547,13 +573,8 @@ lemma dblU_of_Z_eq_zero {P : Fin 3 → R} (hPz : P z = 0) : W'.dblU P = -3 * P x
 
 lemma dblU_ne_zero_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
     (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
-    (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) : W.dblU P ≠ 0 := by
-  rw [nonsingular_of_Z_ne_zero hPz, Affine.Nonsingular, ← equation_of_Z_ne_zero hPz,
-    ← eval_polynomialX_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 4 hPz,
-    ← eval_polynomialY_of_Z_ne_zero hPz, div_ne_zero_iff, and_iff_left <| pow_ne_zero 3 hPz,
-    show eval P W.polynomialY = P y - W.negY P by rw [negY, eval_polynomialY]; ring1,
-    Y_eq_negY_of_Y_eq hQz hx hy hy', sub_self, ne_self_iff_false, or_false] at hP
-  exact hP.right
+    (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) : W.dblU P ≠ 0 :=
+  ((nonsingular_iff_of_Y_eq_negY hPz <| Y_eq_negY_of_Y_eq hQz hx hy hy').mp hP).right
 
 lemma isUnit_dblU_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
     (hx : P x * Q z ^ 2 = Q x * P z ^ 2) (hy : P y * Q z ^ 3 = Q y * P z ^ 3)
@@ -776,6 +797,8 @@ lemma isUnit_addU_of_Y_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0
 def addZ (P Q : Fin 3 → R) : R :=
   P x * Q z ^ 2 - Q x * P z ^ 2
 
+lemma addZ_self {P : Fin 3 → R} : addZ P P = 0 := sub_self _
+
 lemma addZ_smul (P Q : Fin 3 → R) (u v : R) : addZ (u • P) (v • Q) = (u * v) ^ 2 * addZ P Q := by
   simp only [addZ, smul_fin3_ext]
   ring1
@@ -818,6 +841,9 @@ def addX (P Q : Fin 3 → R) : R :=
     - W'.a₃ * P y * P z * Q z ^ 4 + W'.a₄ * Q x * P z ^ 4 * Q z ^ 2
     + W'.a₄ * P x * P z ^ 2 * Q z ^ 4 + 2 * W'.a₆ * P z ^ 4 * Q z ^ 4
 
+lemma addX_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P P = 0 := by
+  linear_combination (norm := (rw [addX]; ring1)) -2 * P z ^ 2 * (equation_iff _).mp hP
+
 lemma addX_eq' {P Q : Fin 3 → R} (hP : W'.Equation P) (hQ : W'.Equation Q) :
     W'.addX P Q * (P z * Q z) ^ 2 =
       (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
@@ -888,6 +914,8 @@ def negAddY (P Q : Fin 3 → R) : R :=
     + W'.a₄ * P x * P y * P z * Q z ^ 6 - 2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3
     + 2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6
 
+lemma negAddY_self {P : Fin 3 → R} : W'.negAddY P P = 0 := by rw [negAddY]; ring
+
 lemma negAddY_eq' {P Q : Fin 3 → R} : W'.negAddY P Q * (P z * Q z) ^ 3 =
     (P y * Q z ^ 3 - Q y * P z ^ 3) * (W'.addX P Q * (P z * Q z) ^ 2 - P x * Q z ^ 2 * addZ P Q ^ 2)
       + P y * Q z ^ 3 * addZ P Q ^ 3 := by
@@ -947,6 +975,9 @@ variable (W') in
 def addY (P Q : Fin 3 → R) : R :=
   W'.negY ![W'.addX P Q, W'.negAddY P Q, addZ P Q]
 
+lemma addY_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P P = 0 := by
+  erw [addY, addX_self hP, negAddY_self, addZ_self, negY_of_Z_eq_zero rfl, neg_zero]
+
 lemma addY_smul (P Q : Fin 3 → R) (u v : R) :
     W'.addY (u • P) (v • Q) = ((u * v) ^ 2) ^ 3 * W'.addY P Q := by
   simp only [addY, negY, addX_smul, negAddY_smul, addZ_smul, fin3_def_ext]
@@ -987,6 +1018,9 @@ variable (W') in
 noncomputable def addXYZ (P Q : Fin 3 → R) : Fin 3 → R :=
   ![W'.addX P Q, W'.addY P Q, addZ P Q]
 
+lemma addXYZ_self {P : Fin 3 → R} (hP : W'.Equation P) : W'.addXYZ P P = ![0, 0, 0] := by
+  rw [addXYZ, addX_self hP, addY_self hP, addZ_self]
+
 lemma addXYZ_smul (P Q : Fin 3 → R) (u v : R) :
     W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q := by
   rw [addXYZ, addX_smul, addY_smul, addZ_smul]
@@ -1068,6 +1102,26 @@ lemma nonsingular_neg {P : Fin 3 → F} (hP : W.Nonsingular P) : W.Nonsingular <
   · simp only [neg_of_Z_ne_zero hPz, nonsingular_smul _ <| Ne.isUnit hPz,
       nonsingular_neg_of_Z_ne_zero hP hPz]
 
+lemma addZ_neg {P : Fin 3 → R} : addZ P (W'.neg P) = 0 := addZ_of_X_eq rfl
+
+lemma addX_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P (W'.neg P) = W'.dblZ P ^ 2 := by
+  simp only [addX, neg, dblZ, negY, fin3_def_ext]
+  linear_combination -2 * P z ^ 2 * (equation_iff _).mp hP
+
+lemma negAddY_neg {P : Fin 3 → R} (hP : W'.Equation P) :
+    W'.negAddY P (W'.neg P) = W'.dblZ P ^ 3 := by
+  simp only [negAddY, neg, dblZ, negY, fin3_def_ext]
+  linear_combination -2 * (2 * P y * P z ^ 3 + W'.a₁ * P x * P z ^ 4 + W'.a₃ * P z ^ 6)
+    * (equation_iff _).mp hP
+
+lemma addY_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addY P (W'.neg P) = -W'.dblZ P ^ 3 := by
+  rw [addY, addX_neg hP, negAddY_neg hP, negY_of_Z_eq_zero addZ_neg]; rfl
+
+lemma addXYZ_neg {P : Fin 3 → R} (hP : W'.Equation P) :
+    W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0] := by
+  erw [addXYZ, addX_neg hP, addY_neg hP, addZ_neg, smul_fin3, neg_sq, mul_one,
+    Odd.neg_pow <| by decide, mul_one, mul_zero]
+
 variable (W') in
 /-- The negation of a point class. If `P` is a point representative,
 then `W'.negMap ⟦P⟧` is definitionally equivalent to `W'.neg P`. -/
@@ -1318,6 +1372,11 @@ lemma fromAffine_some [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y)
     fromAffine (.some h) = ⟨(nonsingularLift_some ..).mpr h⟩ :=
   rfl
 
+lemma fromAffine_ne_zero [Nontrivial R] {X Y : R} (h : W'.toAffine.Nonsingular X Y) :
+    fromAffine (.some h) ≠ 0 := fun h0 ↦ by
+  obtain ⟨u, eq⟩ := Quotient.eq.mp <| (Point.ext_iff ..).mp h0
+  simpa [Units.smul_def, smul_fin3] using congr_fun eq z
+
 /-- The negation of a nonsingular rational point on `W`.
 Given a nonsingular rational point `P` on `W`, use `-P` instead of `neg P`. -/
 def neg (P : W.Point) : W.Point :=
@@ -1503,6 +1562,53 @@ end Point
 
 end Affine
 
+section Map
+
+variable {S : Type*} [CommRing S] (f : R →+* S) (P Q : Fin 3 → R)
+
+protected lemma map_smul (u : R) : f ∘ (u • P) = f u • (f ∘ P) := by
+  ext i; fin_cases i <;> simp [smul_fin3]
+
+@[simp] lemma map_addZ : addZ (f ∘ P) (f ∘ Q) = f (addZ P Q) := by simp [addZ]
+@[simp] lemma map_addX : addX (W'.map f) (f ∘ P) (f ∘ Q) = f (W'.addX P Q) := by simp [addX]
+@[simp] lemma map_negAddY : negAddY (W'.map f) (f ∘ P) (f ∘ Q) = f (W'.negAddY P Q) := by
+  simp [negAddY]
+@[simp] lemma map_negY : negY (W'.map f) (f ∘ P) = f (W'.negY P) := by simp [negY]
+
+@[simp] protected lemma map_neg : neg (W'.map f) (f ∘ P) = f ∘ W'.neg P := by
+  ext i; fin_cases i <;> simp [neg]
+
+@[simp] lemma map_addY : addY (W'.map f) (f ∘ P) (f ∘ Q) = f (W'.addY P Q) := by
+  simp [addY, ← comp_fin3]
+
+@[simp] lemma map_addXYZ : addXYZ (W'.map f) (f ∘ P) (f ∘ Q) = f ∘ addXYZ W' P Q := by
+  simp_rw [addXYZ, comp_fin3, map_addX, map_addY, map_addZ]
+
+lemma map_polynomial : (W'.map f).toJacobian.polynomial = MvPolynomial.map f W'.polynomial := by
+  simp [polynomial]
+
+lemma map_polynomialX : (W'.map f).toJacobian.polynomialX = MvPolynomial.map f W'.polynomialX := by
+  simp [polynomialX, map_polynomial, pderiv_map]
+
+lemma map_polynomialY : (W'.map f).toJacobian.polynomialY = MvPolynomial.map f W'.polynomialY := by
+  simp [polynomialY, map_polynomial, pderiv_map]
+
+lemma map_polynomialZ : (W'.map f).toJacobian.polynomialZ = MvPolynomial.map f W'.polynomialZ := by
+  simp [polynomialZ, map_polynomial, pderiv_map]
+
+@[simp] lemma map_dblZ : dblZ (W'.map f) (f ∘ P) = f (W'.dblZ P) := by simp [dblZ]
+@[simp] lemma map_dblU : dblU (W'.map f) (f ∘ P) = f (W'.dblU P) := by
+  simp [dblU, map_polynomialX, ← eval₂_id, eval₂_comp_left]
+
+@[simp] lemma map_dblX : dblX (W'.map f) (f ∘ P) = f (W'.dblX P) := by simp [dblX]
+@[simp] lemma map_negDblY : negDblY (W'.map f) (f ∘ P) = f (W'.negDblY P) := by simp [negDblY]
+@[simp] lemma map_dblY : dblY (W'.map f) (f ∘ P) = f (W'.dblY P) := by simp [dblY, ← comp_fin3]
+
+@[simp] lemma map_dblXYZ : dblXYZ (W'.map f) (f ∘ P) = f ∘ dblXYZ W' P := by
+  simp_rw [dblXYZ, comp_fin3, map_dblX, map_dblY, map_dblZ]
+
+end Map
+
 end WeierstrassCurve.Jacobian
 
 /-- An abbreviation for `WeierstrassCurve.Jacobian.Point.fromAffine` for dot notation. -/