From 906e8581e77684f8c4425ddf76f9cd0070395cbd Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Thu, 4 Jan 2024 09:48:58 +0000 Subject: [PATCH 1/5] Implement equations and nonsingularity for Jacobian coordinates --- Mathlib.lean | 1 + .../EllipticCurve/Jacobian.lean | 314 ++++++++++++++++++ 2 files changed, 315 insertions(+) create mode 100644 Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean diff --git a/Mathlib.lean b/Mathlib.lean index 72f713857128d..65cf3ba1d377b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -492,6 +492,7 @@ import Mathlib.Algebra.Tropical.Lattice import Mathlib.AlgebraicGeometry.AffineScheme import Mathlib.AlgebraicGeometry.EllipticCurve.Affine import Mathlib.AlgebraicGeometry.EllipticCurve.Group +import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass import Mathlib.AlgebraicGeometry.FunctionField import Mathlib.AlgebraicGeometry.GammaSpecAdjunction diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean new file mode 100644 index 0000000000000..1d779115ee030 --- /dev/null +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -0,0 +1,314 @@ +/- +Copyright (c) 2023 David Kurniadi Angdinata. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: David Kurniadi Angdinata +-/ +import Mathlib.AlgebraicGeometry.EllipticCurve.Affine +import Mathlib.Data.MvPolynomial.CommRing + +/-! +# Jacobian coordinates for Weierstrass curves + +This file defines the type of points on a Weierstrass curve as a tuple, consisting of an equivalence +class of triples up to scaling by weights, satisfying a Weierstrass equation with a nonsingular +condition. + +## Mathematical background + +Let `W` be a Weierstrass curve over a field `F`. A point on the weighted projective plane with +weights $(2, 3, 1)$ is an equivalence class of triples $[x:y:z]$ with coordinates in `F` such that +$(x, y, z) \sim (x', y', z')$ precisely if there is some unit $u$ of `F` such that +$(x, y, z) = (u^2x', u^3y', uz')$, with an extra condition that $(x, y, z) \ne (0, 0, 0)$. +A rational point is a point on the $(2, 3, 1)$-projective plane satisfying a $(2, 3, 1)$-homogeneous +Weierstrass equation $Y^2 + a_1XYZ + a_3YZ^3 = X^3 + a_2X^2Z^2 + a_4XZ^4 + a_6Z^6$, and being +nonsingular means the partial derivatives $W_X(X, Y, Z)$, $W_Y(X, Y, Z)$, and $W_Z(X, Y, Z)$ do not +vanish simultaneously. Note that the vanishing of the Weierstrass equation and its partial +derivatives are independent of the representative for $[x:y:z]$, and the nonsingularity condition +already implies that $(x, y, z) \ne (0, 0, 0)$, so a nonsingular rational point on `W` can simply be +given by a tuple consisting of $[x:y:z]$ and the nonsingular condition on any representative. +In cryptography, as well as in this file, this is often called the Jacobian coordinates of `W`. + +## Main definitions + + * `WeierstrassCurve.Jacobian.PointClass`: the equivalence class of a point representative. + * `WeierstrassCurve.Jacobian.toAffine`: the Weierstrass curve in affine coordinates. + * `WeierstrassCurve.Jacobian.nonsingular`: the nonsingular condition on a point representative. + * `WeierstrassCurve.Jacobian.nonsingular_lift`: the nonsingular condition on a point class. + +## Implementation notes + +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 auxiliary lemma `fin3_def` 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 again not definitionally equal to `![u² * Q x, u³ * Q y, u * Q z]`, so the +auxiliary lemmas `smul_fin3` and `smul_fin3_ext` can be used to convert between the two forms. + +## References + +[J Silverman, *The Arithmetic of Elliptic Curves*][silverman2009] + +## Tags + +elliptic curve, rational point, Jacobian coordinates +-/ + +local notation "x" => 0 + +local notation "y" => 1 + +local notation "z" => 2 + +local macro "matrix_simp" : tactic => + `(tactic| simp only [Matrix.head_cons, Matrix.tail_cons, Matrix.smul_empty, Matrix.smul_cons, + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two]) + +universe u + +lemma fin3_def {R : Type u} (P : Fin 3 → R) : P = ![P x, P y, P z] := by + ext n; fin_cases n <;> rfl + +private instance {R : Type u} [CommRing R] : SMul Rˣ <| Fin 3 → R := + ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩ + +lemma smul_fin3 {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : + u • P = ![u ^ 2 * P x, u ^ 3 * P y, u * P z] := + rfl + +lemma smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : + (u • P) 0 = u ^ 2 * P x ∧ (u • P) 1 = u ^ 3 * P y ∧ (u • P) 2 = u * P z := + ⟨rfl, rfl, rfl⟩ + +private instance {R : Type u} [CommRing R] : MulAction Rˣ <| Fin 3 → R where + one_smul := fun _ => by + simp only [smul_fin3, Units.val_one, one_pow, one_mul, ← fin3_def] + mul_smul := fun u v P => by + simp only [smul_fin3, Units.val_mul, mul_pow, mul_assoc] + matrix_simp + +/-! ## Weierstrass curves -/ + +/-- An abbreviation for a Weierstrass curve in Jacobian coordinates. -/ +abbrev WeierstrassCurve.Jacobian := + WeierstrassCurve + +namespace WeierstrassCurve.Jacobian + +open MvPolynomial + +local macro "eval_simp" : tactic => + `(tactic| simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, eval_pow]) + +variable (R : Type u) [CommRing R] + +/-- The equivalence setoid for a point representative. -/ +def PointSetoid : Setoid <| Fin 3 → R := + MulAction.orbitRel Rˣ <| Fin 3 → R + +attribute [local instance] PointSetoid + +/-- The equivalence class of a point representative. -/ +abbrev PointClass : Type u := + MulAction.orbitRel.Quotient Rˣ <| Fin 3 → R + +variable {R} (W : Jacobian R) + +/-- The coercion to a Weierstrass curve in affine coordinates. -/ +@[pp_dot] +abbrev toAffine : Affine R := + W + +section Equation + +/-! ### Equations and nonsingularity -/ + +/-- The polynomial $W(X, Y, Z) := Y^2 + a_1XYZ + a_3YZ^3 - (X^3 + a_2X^2Z^2 + a_4XZ^4 + a_6Z^6)$ +associated to a Weierstrass curve `W` over `R`. 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. -/ +@[pp_dot] +noncomputable def polynomial : MvPolynomial (Fin 3) R := + X 1 ^ 2 + C W.a₁ * X 0 * X 1 * X 2 + C W.a₃ * X 1 * X 2 ^ 3 + - (X 0 ^ 3 + C W.a₂ * X 0 ^ 2 * X 2 ^ 2 + C W.a₄ * X 0 * X 2 ^ 4 + C W.a₆ * X 2 ^ 6) + +lemma eval_polynomial (P : Fin 3 → R) : eval P W.polynomial = + P y ^ 2 + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 3 + - (P x ^ 3 + W.a₂ * P x ^ 2 * P z ^ 2 + W.a₄ * P x * P z ^ 4 + W.a₆ * P z ^ 6) := by + rw [polynomial] + eval_simp + +/-- The proposition that a point representative $(x, y, z)$ lies in `W`. +In other words, $W(x, y, z) = 0$. -/ +@[pp_dot] +def equation (P : Fin 3 → R) : Prop := + eval P W.polynomial = 0 + +lemma equation_iff (P : Fin 3 → R) : W.equation P ↔ + P y ^ 2 + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 3 + = P x ^ 3 + W.a₂ * P x ^ 2 * P z ^ 2 + W.a₄ * P x * P z ^ 4 + W.a₆ * P z ^ 6 := by + rw [equation, eval_polynomial, sub_eq_zero] + +lemma equation_zero : W.equation ![1, 1, 0] := + (W.equation_iff ![1, 1, 0]).mpr <| by matrix_simp; ring1 + +lemma equation_zero' (Y : R) : W.equation ![Y ^ 2, Y ^ 3, 0] := + (W.equation_iff ![Y ^ 2, Y ^ 3, 0]).mpr <| by matrix_simp; ring1 + +lemma equation_some (X Y : R) : W.equation ![X, Y, 1] ↔ W.toAffine.equation X Y := by + rw [equation_iff, W.toAffine.equation_iff] + congr! 1 <;> matrix_simp <;> ring1 + +lemma equation_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.equation (u • P) ↔ W.equation P := + have (u : Rˣ) {P : Fin 3 → R} (h : W.equation P) : W.equation <| u • P := by + rw [equation_iff] at h ⊢ + linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) (u : R) ^ 6 * h + ⟨fun h => by convert this u⁻¹ h; rw [inv_smul_smul], this u⟩ + +/-- The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$. + +TODO: define this in terms of `MvPolynomial.pderiv`. -/ +@[pp_dot] +noncomputable def polynomialX : MvPolynomial (Fin 3) R := + C W.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W.a₂) * X 0 * X 2 ^ 2 + C W.a₄ * X 2 ^ 4) + +lemma eval_polynomialX (P : Fin 3 → R) : eval P W.polynomialX = + W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4) := by + rw [polynomialX] + eval_simp + +/-- The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$. + +TODO: define this in terms of `MvPolynomial.pderiv`. -/ +@[pp_dot] +noncomputable def polynomialY : MvPolynomial (Fin 3) R := + C 2 * X 1 + C W.a₁ * X 0 * X 2 + C W.a₃ * X 2 ^ 3 + +lemma eval_polynomialY (P : Fin 3 → R) : + eval P W.polynomialY = 2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3 := by + rw [polynomialY] + eval_simp + +/-- The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$. + +TODO: define this in terms of `MvPolynomial.pderiv`. -/ +@[pp_dot] +noncomputable def polynomialZ : MvPolynomial (Fin 3) R := + C W.a₁ * X 0 * X 1 + C (3 * W.a₃) * X 1 * X 2 ^ 2 + - (C (2 * W.a₂) * X 0 ^ 2 * X 2 + C (4 * W.a₄) * X 0 * X 2 ^ 3 + C (6 * W.a₆) * X 2 ^ 5) + +lemma eval_polynomialZ (P : Fin 3 → R) : eval P W.polynomialZ = + W.a₁ * P x * P y + 3 * W.a₃ * P y * P z ^ 2 + - (2 * W.a₂ * P x ^ 2 * P z + 4 * W.a₄ * P x * P z ^ 3 + 6 * W.a₆ * P z ^ 5) := by + rw [polynomialZ] + eval_simp + +/-- The proposition that a point representative $(x, y, z)$ in `W` is nonsingular. +In other words, either $W_X(x, y, z) \ne 0$, $W_Y(x, y, z) \ne 0$, or $W_Z(x, y, z) \ne 0$. -/ +@[pp_dot] +def nonsingular (P : Fin 3 → R) : Prop := + W.equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0 ∨ eval P W.polynomialZ ≠ 0) + +lemma nonsingular_iff (P : Fin 3 → R) : W.nonsingular P ↔ W.equation P ∧ + (W.a₁ * P y * P z ≠ 3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4 ∨ + P y ≠ -P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3 ∨ + W.a₁ * P x * P y + 3 * W.a₃ * P y * P z ^ 2 + ≠ 2 * W.a₂ * P x ^ 2 * P z + 4 * W.a₄ * P x * P z ^ 3 + 6 * W.a₆ * P z ^ 5) := by + rw [nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ, sub_ne_zero, sub_ne_zero, + ← sub_ne_zero (a := P y)] + congr! 4 + ring1 + +lemma nonsingular_zero [Nontrivial R] : W.nonsingular ![1, 1, 0] := + (W.nonsingular_iff ![1, 1, 0]).mpr ⟨W.equation_zero, + by simp; by_contra! h; exact one_ne_zero <| by linear_combination -h.1 - h.2.1⟩ + +lemma nonsingular_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : + W.nonsingular ![Y ^ 2, Y ^ 3, 0] := + (W.nonsingular_iff ![Y ^ 2, Y ^ 3, 0]).mpr ⟨W.equation_zero' Y, + by simp [hy]; by_contra! h; exact pow_ne_zero 3 hy <| by linear_combination Y ^ 3 * h.1 - h.2.1⟩ + +lemma nonsingular_some (X Y : R) : W.nonsingular ![X, Y, 1] ↔ W.toAffine.nonsingular X Y := by + rw [nonsingular_iff] + matrix_simp + simp only [W.toAffine.nonsingular_iff, equation_some, and_congr_right_iff, + W.toAffine.equation_iff, ← not_and_or, not_iff_not, one_pow, mul_one, Iff.comm, iff_self_and] + intro h hX hY + linear_combination (norm := ring1) 6 * h - 2 * X * hX - 3 * Y * hY + +lemma nonsingular_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.nonsingular (u • P) ↔ W.nonsingular P := + have (u : Rˣ) {P : Fin 3 → R} (h : W.nonsingular <| u • P) : W.nonsingular P := by + rcases (W.nonsingular_iff _).mp h with ⟨h, h'⟩ + refine (W.nonsingular_iff P).mpr ⟨(W.equation_smul_iff P u).mp h, ?_⟩ + contrapose! h' + simp only [smul_fin3_ext] + exact ⟨by linear_combination (norm := ring1) (u : R) ^ 4 * h'.left, + by linear_combination (norm := ring1) (u : R) ^ 3 * h'.right.left, + by linear_combination (norm := ring1) (u : R) ^ 5 * h'.right.right⟩ + ⟨this u, fun h => this u⁻¹ <| by rwa [inv_smul_smul]⟩ + +lemma nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W.nonsingular P ↔ W.nonsingular Q := by + rcases h with ⟨u, rfl⟩ + exact W.nonsingular_smul_iff Q u + +/-- The proposition that a point class on `W` is nonsingular. If `P` is a point representative, +then `W.nonsingular_lift ⟦P⟧` is definitionally equivalent to `W.nonsingular P`. -/ +@[pp_dot] +def nonsingular_lift (P : PointClass R) : Prop := + P.lift W.nonsingular fun _ _ => propext ∘ W.nonsingular_of_equiv + +@[simp] +lemma nonsingular_lift_eq (P : Fin 3 → R) : W.nonsingular_lift ⟦P⟧ = W.nonsingular P := + rfl + +lemma nonsingular_lift_zero [Nontrivial R] : W.nonsingular_lift ⟦![1, 1, 0]⟧ := + W.nonsingular_zero + +lemma nonsingular_lift_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : + W.nonsingular_lift ⟦![Y ^ 2, Y ^ 3, 0]⟧ := + W.nonsingular_zero' hy + +lemma nonsingular_lift_some (X Y : R) : + W.nonsingular_lift ⟦![X, Y, 1]⟧ ↔ W.toAffine.nonsingular X Y := + W.nonsingular_some X Y + +variable {F : Type u} [Field F] {W : Jacobian F} + +lemma equiv_of_Zeq0 {P Q : Fin 3 → F} (hP : W.nonsingular P) (hQ : W.nonsingular Q) (hPz : P z = 0) + (hQz : Q z = 0) : P ≈ Q := by + rw [fin3_def P, hPz] at hP ⊢ + rw [fin3_def Q, hQz] at hQ ⊢ + simp [nonsingular_iff, equation_iff] at hP hQ + have hPx : P x ≠ 0 := fun h => by simp [h] at hP; simp [hP] at hP + have hQx : Q x ≠ 0 := fun h => by simp [h] at hQ; simp [hQ] at hQ + have hPy : P y ≠ 0 := fun h => by simp [h] at hP; exact hPx <| pow_eq_zero hP.left.symm + have hQy : Q y ≠ 0 := fun h => by simp [h] at hQ; exact hQx <| pow_eq_zero hQ.left.symm + use Units.mk0 _ <| mul_ne_zero (div_ne_zero hPy hPx) (div_ne_zero hQx hQy) + simp [smul_fin3, mul_pow, div_pow] + congr! 2 + · field_simp [hP.left, hQ.left] + ring1 + · field_simp [← hP.left, ← hQ.left] + ring1 + +lemma equiv_zero_of_Zeq0 {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z = 0) : P ≈ ![1, 1, 0] := + equiv_of_Zeq0 h W.nonsingular_zero hPz rfl + +lemma equiv_some_of_Zne0 {P : Fin 3 → F} (hPz : P z ≠ 0) : P ≈ ![P x / P z ^ 2, P y / P z ^ 3, 1] := + ⟨Units.mk0 _ hPz, by simp [smul_fin3, ← fin3_def P, mul_div_cancel' _ <| pow_ne_zero _ hPz]⟩ + +lemma nonsingular_iff_affine_of_Zne0 {P : Fin 3 → F} (hPz : P z ≠ 0) : + W.nonsingular P ↔ W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3) := + (W.nonsingular_of_equiv <| equiv_some_of_Zne0 hPz).trans <| W.nonsingular_some .. + +lemma nonsingular_of_affine_of_Zne0 {P : Fin 3 → F} + (h : W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3)) (hPz : P z ≠ 0) : + W.nonsingular P := + (nonsingular_iff_affine_of_Zne0 hPz).mpr h + +lemma nonsingular_affine_of_Zne0 {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z ≠ 0) : + W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3) := + (nonsingular_iff_affine_of_Zne0 hPz).mp h + +end Equation + +end WeierstrassCurve.Jacobian From 3e389af4be23c2bc4221224f46b8dd493efb1f25 Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Mon, 15 Jan 2024 21:31:30 +0000 Subject: [PATCH 2/5] Replace numerals with notation --- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index 1d779115ee030..2b02ddc1497a4 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -77,7 +77,7 @@ lemma smul_fin3 {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : rfl lemma smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : - (u • P) 0 = u ^ 2 * P x ∧ (u • P) 1 = u ^ 3 * P y ∧ (u • P) 2 = u * P z := + (u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z := ⟨rfl, rfl, rfl⟩ private instance {R : Type u} [CommRing R] : MulAction Rˣ <| Fin 3 → R where From 6ed760c717a7772d7e5a16e6bc3d82eff7919c5f Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Mon, 19 Feb 2024 15:32:14 +0000 Subject: [PATCH 3/5] Apply suggestions --- .../EllipticCurve/Jacobian.lean | 130 ++++++++++-------- Mathlib/Data/MvPolynomial/PDeriv.lean | 4 + 2 files changed, 77 insertions(+), 57 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index 2b02ddc1497a4..16ba302585abf 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -5,6 +5,7 @@ Authors: David Kurniadi Angdinata -/ import Mathlib.AlgebraicGeometry.EllipticCurve.Affine import Mathlib.Data.MvPolynomial.CommRing +import Mathlib.Data.MvPolynomial.PDeriv /-! # Jacobian coordinates for Weierstrass curves @@ -62,58 +63,59 @@ local notation "z" => 2 local macro "matrix_simp" : tactic => `(tactic| simp only [Matrix.head_cons, Matrix.tail_cons, Matrix.smul_empty, Matrix.smul_cons, - Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two]) + Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two]) universe u -lemma fin3_def {R : Type u} (P : Fin 3 → R) : P = ![P x, P y, P z] := by +/-! ## Weierstrass curves -/ + +/-- An abbreviation for a Weierstrass curve in Jacobian coordinates. -/ +abbrev WeierstrassCurve.Jacobian := + WeierstrassCurve + +namespace WeierstrassCurve.Jacobian + +open MvPolynomial + +local macro "eval_simp" : tactic => + `(tactic| simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, eval_pow]) + +local macro "pderiv_simp" : tactic => + `(tactic| simp only [map_ofNat, map_neg, map_add, map_sub, map_mul, pderiv_mul, pderiv_pow, + pderiv_C, pderiv_X_self, pderiv_X_of_ne one_ne_zero, pderiv_X_of_ne one_ne_zero.symm, + pderiv_X_of_ne (by decide : (2 : Fin 3) ≠ 0), pderiv_X_of_ne (by decide : (0 : Fin 3) ≠ 2), + pderiv_X_of_ne (by decide : (2 : Fin 3) ≠ 1), pderiv_X_of_ne (by decide : (1 : Fin 3) ≠ 2)]) + +variable {R : Type u} [CommRing R] (W : Jacobian R) + +lemma fin3_def (P : Fin 3 → R) : P = ![P x, P y, P z] := by ext n; fin_cases n <;> rfl -private instance {R : Type u} [CommRing R] : SMul Rˣ <| Fin 3 → R := +scoped instance instSMulPoint : SMul Rˣ <| Fin 3 → R := ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩ -lemma smul_fin3 {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : +lemma smul_fin3 (P : Fin 3 → R) (u : Rˣ) : u • P = ![u ^ 2 * P x, u ^ 3 * P y, u * P z] := rfl -lemma smul_fin3_ext {R : Type u} [CommRing R] (P : Fin 3 → R) (u : Rˣ) : +lemma smul_fin3_ext (P : Fin 3 → R) (u : Rˣ) : (u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z := ⟨rfl, rfl, rfl⟩ -private instance {R : Type u} [CommRing R] : MulAction Rˣ <| Fin 3 → R where +scoped instance instMulActionPoint : MulAction Rˣ <| Fin 3 → R where one_smul := fun _ => by simp only [smul_fin3, Units.val_one, one_pow, one_mul, ← fin3_def] mul_smul := fun u v P => by simp only [smul_fin3, Units.val_mul, mul_pow, mul_assoc] matrix_simp -/-! ## Weierstrass curves -/ - -/-- An abbreviation for a Weierstrass curve in Jacobian coordinates. -/ -abbrev WeierstrassCurve.Jacobian := - WeierstrassCurve - -namespace WeierstrassCurve.Jacobian - -open MvPolynomial - -local macro "eval_simp" : tactic => - `(tactic| simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, eval_pow]) - -variable (R : Type u) [CommRing R] - -/-- The equivalence setoid for a point representative. -/ -def PointSetoid : Setoid <| Fin 3 → R := +scoped instance instSetoidPoint : Setoid <| Fin 3 → R := MulAction.orbitRel Rˣ <| Fin 3 → R -attribute [local instance] PointSetoid - /-- The equivalence class of a point representative. -/ -abbrev PointClass : Type u := +abbrev PointClass (R : Type u) [CommRing R] : Type u := MulAction.orbitRel.Quotient Rˣ <| Fin 3 → R -variable {R} (W : Jacobian R) - /-- The coercion to a Weierstrass curve in affine coordinates. -/ @[pp_dot] abbrev toAffine : Affine R := @@ -164,42 +166,54 @@ lemma equation_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.equation (u • P) ↔ W linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) (u : R) ^ 6 * h ⟨fun h => by convert this u⁻¹ h; rw [inv_smul_smul], this u⟩ -/-- The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$. - -TODO: define this in terms of `MvPolynomial.pderiv`. -/ +/-- The partial derivative $W_X(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $X$. -/ @[pp_dot] noncomputable def polynomialX : MvPolynomial (Fin 3) R := - C W.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W.a₂) * X 0 * X 2 ^ 2 + C W.a₄ * X 2 ^ 4) + pderiv x W.polynomial + +lemma polynomialX_eq : W.polynomialX = + C W.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W.a₂) * X 0 * X 2 ^ 2 + C W.a₄ * X 2 ^ 4) := by + rw [polynomialX, polynomial] + pderiv_simp + ring1 lemma eval_polynomialX (P : Fin 3 → R) : eval P W.polynomialX = W.a₁ * P y * P z - (3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4) := by - rw [polynomialX] + rw [polynomialX_eq] eval_simp -/-- The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$. - -TODO: define this in terms of `MvPolynomial.pderiv`. -/ +/-- The partial derivative $W_Y(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Y$. -/ @[pp_dot] noncomputable def polynomialY : MvPolynomial (Fin 3) R := - C 2 * X 1 + C W.a₁ * X 0 * X 2 + C W.a₃ * X 2 ^ 3 + pderiv y W.polynomial + +lemma polynomialY_eq : W.polynomialY = + C 2 * X 1 + C W.a₁ * X 0 * X 2 + C W.a₃ * X 2 ^ 3 := by + rw [polynomialY, polynomial] + pderiv_simp + ring1 lemma eval_polynomialY (P : Fin 3 → R) : eval P W.polynomialY = 2 * P y + W.a₁ * P x * P z + W.a₃ * P z ^ 3 := by - rw [polynomialY] + rw [polynomialY_eq] eval_simp -/-- The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$. - -TODO: define this in terms of `MvPolynomial.pderiv`. -/ +/-- The partial derivative $W_Z(X, Y, Z)$ of $W(X, Y, Z)$ with respect to $Z$. -/ @[pp_dot] noncomputable def polynomialZ : MvPolynomial (Fin 3) R := - C W.a₁ * X 0 * X 1 + C (3 * W.a₃) * X 1 * X 2 ^ 2 - - (C (2 * W.a₂) * X 0 ^ 2 * X 2 + C (4 * W.a₄) * X 0 * X 2 ^ 3 + C (6 * W.a₆) * X 2 ^ 5) + pderiv z W.polynomial + +lemma polynomialZ_eq : W.polynomialZ = + C W.a₁ * X 0 * X 1 + C (3 * W.a₃) * X 1 * X 2 ^ 2 + - (C (2 * W.a₂) * X 0 ^ 2 * X 2 + C (4 * W.a₄) * X 0 * X 2 ^ 3 + C (6 * W.a₆) * X 2 ^ 5) := by + rw [polynomialZ, polynomial] + pderiv_simp + ring1 lemma eval_polynomialZ (P : Fin 3 → R) : eval P W.polynomialZ = W.a₁ * P x * P y + 3 * W.a₃ * P y * P z ^ 2 - (2 * W.a₂ * P x ^ 2 * P z + 4 * W.a₄ * P x * P z ^ 3 + 6 * W.a₆ * P z ^ 5) := by - rw [polynomialZ] + rw [polynomialZ_eq] eval_simp /-- The proposition that a point representative $(x, y, z)$ in `W` is nonsingular. @@ -257,8 +271,8 @@ def nonsingular_lift (P : PointClass R) : Prop := P.lift W.nonsingular fun _ _ => propext ∘ W.nonsingular_of_equiv @[simp] -lemma nonsingular_lift_eq (P : Fin 3 → R) : W.nonsingular_lift ⟦P⟧ = W.nonsingular P := - rfl +lemma nonsingular_lift_iff (P : Fin 3 → R) : W.nonsingular_lift ⟦P⟧ ↔ W.nonsingular P := + Iff.rfl lemma nonsingular_lift_zero [Nontrivial R] : W.nonsingular_lift ⟦![1, 1, 0]⟧ := W.nonsingular_zero @@ -273,8 +287,8 @@ lemma nonsingular_lift_some (X Y : R) : variable {F : Type u} [Field F] {W : Jacobian F} -lemma equiv_of_Zeq0 {P Q : Fin 3 → F} (hP : W.nonsingular P) (hQ : W.nonsingular Q) (hPz : P z = 0) - (hQz : Q z = 0) : P ≈ Q := by +lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.nonsingular P) (hQ : W.nonsingular Q) + (hPz : P z = 0) (hQz : Q z = 0) : P ≈ Q := by rw [fin3_def P, hPz] at hP ⊢ rw [fin3_def Q, hQz] at hQ ⊢ simp [nonsingular_iff, equation_iff] at hP hQ @@ -290,24 +304,26 @@ lemma equiv_of_Zeq0 {P Q : Fin 3 → F} (hP : W.nonsingular P) (hQ : W.nonsingul · field_simp [← hP.left, ← hQ.left] ring1 -lemma equiv_zero_of_Zeq0 {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z = 0) : P ≈ ![1, 1, 0] := - equiv_of_Zeq0 h W.nonsingular_zero hPz rfl +lemma equiv_zero_of_Z_eq_zero {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z = 0) : + P ≈ ![1, 1, 0] := + equiv_of_Z_eq_zero h W.nonsingular_zero hPz rfl -lemma equiv_some_of_Zne0 {P : Fin 3 → F} (hPz : P z ≠ 0) : P ≈ ![P x / P z ^ 2, P y / P z ^ 3, 1] := +lemma equiv_some_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : + P ≈ ![P x / P z ^ 2, P y / P z ^ 3, 1] := ⟨Units.mk0 _ hPz, by simp [smul_fin3, ← fin3_def P, mul_div_cancel' _ <| pow_ne_zero _ hPz]⟩ -lemma nonsingular_iff_affine_of_Zne0 {P : Fin 3 → F} (hPz : P z ≠ 0) : +lemma nonsingular_iff_affine_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) := - (W.nonsingular_of_equiv <| equiv_some_of_Zne0 hPz).trans <| W.nonsingular_some .. + (W.nonsingular_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| W.nonsingular_some .. -lemma nonsingular_of_affine_of_Zne0 {P : Fin 3 → F} +lemma nonsingular_of_affine_of_Z_ne_zero {P : Fin 3 → F} (h : W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3)) (hPz : P z ≠ 0) : W.nonsingular P := - (nonsingular_iff_affine_of_Zne0 hPz).mpr h + (nonsingular_iff_affine_of_Z_ne_zero hPz).mpr h -lemma nonsingular_affine_of_Zne0 {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z ≠ 0) : +lemma nonsingular_affine_of_Z_ne_zero {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z ≠ 0) : W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3) := - (nonsingular_iff_affine_of_Zne0 hPz).mp h + (nonsingular_iff_affine_of_Z_ne_zero hPz).mp h end Equation diff --git a/Mathlib/Data/MvPolynomial/PDeriv.lean b/Mathlib/Data/MvPolynomial/PDeriv.lean index 1612bc4690226..47d25f7a10a7a 100644 --- a/Mathlib/Data/MvPolynomial/PDeriv.lean +++ b/Mathlib/Data/MvPolynomial/PDeriv.lean @@ -119,6 +119,10 @@ theorem pderiv_mul {i : σ} {f g : MvPolynomial σ R} : simp only [(pderiv i).leibniz f g, smul_eq_mul, mul_comm, add_comm] #align mv_polynomial.pderiv_mul MvPolynomial.pderiv_mul +theorem pderiv_pow {i : σ} {f : MvPolynomial σ R} {n : ℕ} : + pderiv i (f ^ n) = n * f ^ (n - 1) * pderiv i f := by + rw [(pderiv i).leibniz_pow f n, nsmul_eq_mul, smul_eq_mul, mul_assoc] + -- @[simp] -- Porting note: simp can prove this theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f := by rw [C_mul', Derivation.map_smul, C_mul'] From bc4c2685338e3341e985bf62d01d37dea308cc3d Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Mon, 19 Feb 2024 16:06:15 +0000 Subject: [PATCH 4/5] Fix lint --- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index 16ba302585abf..753f280cacecd 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -91,6 +91,7 @@ variable {R : Type u} [CommRing R] (W : Jacobian R) lemma fin3_def (P : Fin 3 → R) : P = ![P x, P y, P z] := by ext n; fin_cases n <;> rfl +/-- 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]⟩ @@ -102,6 +103,7 @@ lemma smul_fin3_ext (P : Fin 3 → R) (u : Rˣ) : (u • P) x = u ^ 2 * P x ∧ (u • P) y = u ^ 3 * P y ∧ (u • P) z = u * P z := ⟨rfl, rfl, rfl⟩ +/-- The multiplicative action on a point representative. -/ scoped instance instMulActionPoint : MulAction Rˣ <| Fin 3 → R where one_smul := fun _ => by simp only [smul_fin3, Units.val_one, one_pow, one_mul, ← fin3_def] @@ -109,6 +111,7 @@ scoped instance instMulActionPoint : MulAction Rˣ <| Fin 3 → R where simp only [smul_fin3, Units.val_mul, mul_pow, mul_assoc] matrix_simp +/-- The equivalence setoid for a point representative. -/ scoped instance instSetoidPoint : Setoid <| Fin 3 → R := MulAction.orbitRel Rˣ <| Fin 3 → R From 4ac70299f227c94e07880df35bc937362c2c9538 Mon Sep 17 00:00:00 2001 From: David Kurniadi Angdinata Date: Tue, 20 Feb 2024 12:00:57 +0000 Subject: [PATCH 5/5] Rename propositions --- .../EllipticCurve/Jacobian.lean | 75 +++++++++---------- 1 file changed, 36 insertions(+), 39 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean index 753f280cacecd..c7d750c6c60f9 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean @@ -33,8 +33,8 @@ In cryptography, as well as in this file, this is often called the Jacobian coor * `WeierstrassCurve.Jacobian.PointClass`: the equivalence class of a point representative. * `WeierstrassCurve.Jacobian.toAffine`: the Weierstrass curve in affine coordinates. - * `WeierstrassCurve.Jacobian.nonsingular`: the nonsingular condition on a point representative. - * `WeierstrassCurve.Jacobian.nonsingular_lift`: the nonsingular condition on a point class. + * `WeierstrassCurve.Jacobian.Nonsingular`: the nonsingular condition on a point representative. + * `WeierstrassCurve.Jacobian.NonsingularLift`: the nonsingular condition on a point class. ## Implementation notes @@ -105,11 +105,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 := fun _ => by - simp only [smul_fin3, Units.val_one, one_pow, one_mul, ← fin3_def] - mul_smul := fun u v P => by - simp only [smul_fin3, Units.val_mul, mul_pow, mul_assoc] - matrix_simp + one_smul _ := by simp only [smul_fin3, Units.val_one, one_pow, one_mul, ← fin3_def] + mul_smul _ _ _ := by simp only [smul_fin3, Units.val_mul, mul_pow, mul_assoc]; matrix_simp /-- The equivalence setoid for a point representative. -/ scoped instance instSetoidPoint : Setoid <| Fin 3 → R := @@ -145,26 +142,26 @@ lemma eval_polynomial (P : Fin 3 → R) : eval P W.polynomial = /-- The proposition that a point representative $(x, y, z)$ lies in `W`. In other words, $W(x, y, z) = 0$. -/ @[pp_dot] -def equation (P : Fin 3 → R) : Prop := +def Equation (P : Fin 3 → R) : Prop := eval P W.polynomial = 0 -lemma equation_iff (P : Fin 3 → R) : W.equation P ↔ +lemma equation_iff (P : Fin 3 → R) : W.Equation P ↔ P y ^ 2 + W.a₁ * P x * P y * P z + W.a₃ * P y * P z ^ 3 = P x ^ 3 + W.a₂ * P x ^ 2 * P z ^ 2 + W.a₄ * P x * P z ^ 4 + W.a₆ * P z ^ 6 := by - rw [equation, eval_polynomial, sub_eq_zero] + rw [Equation, eval_polynomial, sub_eq_zero] -lemma equation_zero : W.equation ![1, 1, 0] := +lemma equation_zero : W.Equation ![1, 1, 0] := (W.equation_iff ![1, 1, 0]).mpr <| by matrix_simp; ring1 -lemma equation_zero' (Y : R) : W.equation ![Y ^ 2, Y ^ 3, 0] := +lemma equation_zero' (Y : R) : W.Equation ![Y ^ 2, Y ^ 3, 0] := (W.equation_iff ![Y ^ 2, Y ^ 3, 0]).mpr <| by matrix_simp; ring1 -lemma equation_some (X Y : R) : W.equation ![X, Y, 1] ↔ W.toAffine.equation X Y := by +lemma equation_some (X Y : R) : W.Equation ![X, Y, 1] ↔ W.toAffine.equation X Y := by rw [equation_iff, W.toAffine.equation_iff] congr! 1 <;> matrix_simp <;> ring1 -lemma equation_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.equation (u • P) ↔ W.equation P := - have (u : Rˣ) {P : Fin 3 → R} (h : W.equation P) : W.equation <| u • P := by +lemma equation_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.Equation (u • P) ↔ W.Equation P := + have (u : Rˣ) {P : Fin 3 → R} (h : W.Equation P) : W.Equation <| u • P := by rw [equation_iff] at h ⊢ linear_combination (norm := (simp only [smul_fin3_ext]; ring1)) (u : R) ^ 6 * h ⟨fun h => by convert this u⁻¹ h; rw [inv_smul_smul], this u⟩ @@ -222,29 +219,29 @@ lemma eval_polynomialZ (P : Fin 3 → R) : eval P W.polynomialZ = /-- The proposition that a point representative $(x, y, z)$ in `W` is nonsingular. In other words, either $W_X(x, y, z) \ne 0$, $W_Y(x, y, z) \ne 0$, or $W_Z(x, y, z) \ne 0$. -/ @[pp_dot] -def nonsingular (P : Fin 3 → R) : Prop := - W.equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0 ∨ eval P W.polynomialZ ≠ 0) +def Nonsingular (P : Fin 3 → R) : Prop := + W.Equation P ∧ (eval P W.polynomialX ≠ 0 ∨ eval P W.polynomialY ≠ 0 ∨ eval P W.polynomialZ ≠ 0) -lemma nonsingular_iff (P : Fin 3 → R) : W.nonsingular P ↔ W.equation P ∧ +lemma nonsingular_iff (P : Fin 3 → R) : W.Nonsingular P ↔ W.Equation P ∧ (W.a₁ * P y * P z ≠ 3 * P x ^ 2 + 2 * W.a₂ * P x * P z ^ 2 + W.a₄ * P z ^ 4 ∨ P y ≠ -P y - W.a₁ * P x * P z - W.a₃ * P z ^ 3 ∨ W.a₁ * P x * P y + 3 * W.a₃ * P y * P z ^ 2 ≠ 2 * W.a₂ * P x ^ 2 * P z + 4 * W.a₄ * P x * P z ^ 3 + 6 * W.a₆ * P z ^ 5) := by - rw [nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ, sub_ne_zero, sub_ne_zero, + rw [Nonsingular, eval_polynomialX, eval_polynomialY, eval_polynomialZ, sub_ne_zero, sub_ne_zero, ← sub_ne_zero (a := P y)] congr! 4 ring1 -lemma nonsingular_zero [Nontrivial R] : W.nonsingular ![1, 1, 0] := +lemma nonsingular_zero [Nontrivial R] : W.Nonsingular ![1, 1, 0] := (W.nonsingular_iff ![1, 1, 0]).mpr ⟨W.equation_zero, by simp; by_contra! h; exact one_ne_zero <| by linear_combination -h.1 - h.2.1⟩ lemma nonsingular_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : - W.nonsingular ![Y ^ 2, Y ^ 3, 0] := + W.Nonsingular ![Y ^ 2, Y ^ 3, 0] := (W.nonsingular_iff ![Y ^ 2, Y ^ 3, 0]).mpr ⟨W.equation_zero' Y, by simp [hy]; by_contra! h; exact pow_ne_zero 3 hy <| by linear_combination Y ^ 3 * h.1 - h.2.1⟩ -lemma nonsingular_some (X Y : R) : W.nonsingular ![X, Y, 1] ↔ W.toAffine.nonsingular X Y := by +lemma nonsingular_some (X Y : R) : W.Nonsingular ![X, Y, 1] ↔ W.toAffine.nonsingular X Y := by rw [nonsingular_iff] matrix_simp simp only [W.toAffine.nonsingular_iff, equation_some, and_congr_right_iff, @@ -252,8 +249,8 @@ lemma nonsingular_some (X Y : R) : W.nonsingular ![X, Y, 1] ↔ W.toAffine.nonsi intro h hX hY linear_combination (norm := ring1) 6 * h - 2 * X * hX - 3 * Y * hY -lemma nonsingular_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.nonsingular (u • P) ↔ W.nonsingular P := - have (u : Rˣ) {P : Fin 3 → R} (h : W.nonsingular <| u • P) : W.nonsingular P := by +lemma nonsingular_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.Nonsingular (u • P) ↔ W.Nonsingular P := + have (u : Rˣ) {P : Fin 3 → R} (h : W.Nonsingular <| u • P) : W.Nonsingular P := by rcases (W.nonsingular_iff _).mp h with ⟨h, h'⟩ refine (W.nonsingular_iff P).mpr ⟨(W.equation_smul_iff P u).mp h, ?_⟩ contrapose! h' @@ -263,34 +260,34 @@ lemma nonsingular_smul_iff (P : Fin 3 → R) (u : Rˣ) : W.nonsingular (u • P) by linear_combination (norm := ring1) (u : R) ^ 5 * h'.right.right⟩ ⟨this u, fun h => this u⁻¹ <| by rwa [inv_smul_smul]⟩ -lemma nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W.nonsingular P ↔ W.nonsingular Q := by +lemma nonsingular_of_equiv {P Q : Fin 3 → R} (h : P ≈ Q) : W.Nonsingular P ↔ W.Nonsingular Q := by rcases h with ⟨u, rfl⟩ exact W.nonsingular_smul_iff Q u /-- The proposition that a point class on `W` is nonsingular. If `P` is a point representative, -then `W.nonsingular_lift ⟦P⟧` is definitionally equivalent to `W.nonsingular P`. -/ +then `W.NonsingularLift ⟦P⟧` is definitionally equivalent to `W.Nonsingular P`. -/ @[pp_dot] -def nonsingular_lift (P : PointClass R) : Prop := - P.lift W.nonsingular fun _ _ => propext ∘ W.nonsingular_of_equiv +def NonsingularLift (P : PointClass R) : Prop := + P.lift W.Nonsingular fun _ _ => propext ∘ W.nonsingular_of_equiv @[simp] -lemma nonsingular_lift_iff (P : Fin 3 → R) : W.nonsingular_lift ⟦P⟧ ↔ W.nonsingular P := +lemma nonsingularLift_iff (P : Fin 3 → R) : W.NonsingularLift ⟦P⟧ ↔ W.Nonsingular P := Iff.rfl -lemma nonsingular_lift_zero [Nontrivial R] : W.nonsingular_lift ⟦![1, 1, 0]⟧ := +lemma nonsingularLift_zero [Nontrivial R] : W.NonsingularLift ⟦![1, 1, 0]⟧ := W.nonsingular_zero -lemma nonsingular_lift_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : - W.nonsingular_lift ⟦![Y ^ 2, Y ^ 3, 0]⟧ := +lemma nonsingularLift_zero' [NoZeroDivisors R] {Y : R} (hy : Y ≠ 0) : + W.NonsingularLift ⟦![Y ^ 2, Y ^ 3, 0]⟧ := W.nonsingular_zero' hy -lemma nonsingular_lift_some (X Y : R) : - W.nonsingular_lift ⟦![X, Y, 1]⟧ ↔ W.toAffine.nonsingular X Y := +lemma nonsingularLift_some (X Y : R) : + W.NonsingularLift ⟦![X, Y, 1]⟧ ↔ W.toAffine.nonsingular X Y := W.nonsingular_some X Y variable {F : Type u} [Field F] {W : Jacobian F} -lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.nonsingular P) (hQ : W.nonsingular Q) +lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Nonsingular Q) (hPz : P z = 0) (hQz : Q z = 0) : P ≈ Q := by rw [fin3_def P, hPz] at hP ⊢ rw [fin3_def Q, hQz] at hQ ⊢ @@ -307,7 +304,7 @@ lemma equiv_of_Z_eq_zero {P Q : Fin 3 → F} (hP : W.nonsingular P) (hQ : W.nons · field_simp [← hP.left, ← hQ.left] ring1 -lemma equiv_zero_of_Z_eq_zero {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z = 0) : +lemma equiv_zero_of_Z_eq_zero {P : Fin 3 → F} (h : W.Nonsingular P) (hPz : P z = 0) : P ≈ ![1, 1, 0] := equiv_of_Z_eq_zero h W.nonsingular_zero hPz rfl @@ -316,15 +313,15 @@ lemma equiv_some_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) : ⟨Units.mk0 _ hPz, by simp [smul_fin3, ← fin3_def P, mul_div_cancel' _ <| pow_ne_zero _ hPz]⟩ lemma nonsingular_iff_affine_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) := + W.Nonsingular P ↔ W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3) := (W.nonsingular_of_equiv <| equiv_some_of_Z_ne_zero hPz).trans <| W.nonsingular_some .. lemma nonsingular_of_affine_of_Z_ne_zero {P : Fin 3 → F} (h : W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3)) (hPz : P z ≠ 0) : - W.nonsingular P := + W.Nonsingular P := (nonsingular_iff_affine_of_Z_ne_zero hPz).mpr h -lemma nonsingular_affine_of_Z_ne_zero {P : Fin 3 → F} (h : W.nonsingular P) (hPz : P z ≠ 0) : +lemma nonsingular_affine_of_Z_ne_zero {P : Fin 3 → F} (h : W.Nonsingular P) (hPz : P z ≠ 0) : W.toAffine.nonsingular (P x / P z ^ 2) (P y / P z ^ 3) := (nonsingular_iff_affine_of_Z_ne_zero hPz).mp h