wip need more credits

Author: CBirkbeck

Mathlib/Algebra/MvPolynomial/PDeriv.lean

@@ -158,13 +158,6 @@ lemma pderiv_sumToIter {σ ι} (p i) :
   | add p q _ _ => simp_all
   | mul_X p n _ => cases n <;> simp_all [pderiv_X, Pi.single_apply, apply_ite]
 
-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/Affine/Point.lean

@@ -174,6 +174,14 @@ lemma smul_basis_mul_Y (p q : R[X]) : (p • (1 : W'.CoordinateRing) + q • mk
   simp only [smul, add_mul, mul_assoc, ← sq, Y_sq, map_sub, map_mul]
   ring1
 
+lemma algebraMap_poly_injective : Function.Injective (algebraMap R[X] W'.CoordinateRing) :=
+  (injective_iff_map_eq_zero _).mpr fun p hp ↦ And.left <|
+    smul_basis_eq_zero (W' := W') (q := 0) <| by
+      rwa [Algebra.smul_def, mul_one, zero_smul, add_zero]
+
+lemma algebraMap_injective' : Function.Injective (algebraMap R W'.CoordinateRing) :=
+  (CoordinateRing.algebraMap_poly_injective (W' := W')).comp C_injective
+
 variable (W') in
 /-- The ring homomorphism `R[W] →+* S[W.map f]` induced by a ring homomorphism `f : R →+* S`. -/
 noncomputable def map (f : R →+* S) : W'.CoordinateRing →+* (W'.map f).toAffine.CoordinateRing :=
@@ -490,6 +498,10 @@ lemma zero_def : 0 = (.zero : W'.Point) :=
 lemma some_ne_zero {x y : R} (h : W'.Nonsingular x y) : Point.some h ≠ 0 := by
   rintro (_ | _)
 
+lemma some_eq_some_iff {x₁ x₂ y₁ y₂ : R} (h₁ : W'.Nonsingular x₁ y₁)
+    (h₂ : W'.Nonsingular x₂ y₂) : some h₁ = some h₂ ↔ x₁ = x₂ ∧ y₁ = y₂ :=
+  ⟨by rintro (_ | _); trivial, by rintro ⟨rfl, rfl⟩; rfl⟩
+
 /-- The negation of a nonsingular point on a Weierstrass curve in affine coordinates.
 
 Given a nonsingular point `P` in affine coordinates, use `-P` instead of `neg P`. -/

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/ZSMul.lean

@@ -60,7 +60,7 @@ Equivalently, we aim to prove the formula in affine coordinates: `n • (X,Y) =
 for `n ≠ 0` (`Universal.Affine.zsmul_point_eq_smulX_smulY`), but this time it is easier to use
 the usual strong induction on `n` rather than the even-odd induction, because we have formulas
 expressing the affine coordinates of `(n+1) • P` in terms of those of `P`, `n • P` and
-`(n-1) • P` (`Affine.addX_eq_subX_sub`, `Affine.addY_sub_negY`).
+`(n-1) • P` (`Affine.addX_eq_addX_negY_sub`, `Affine.addY_sub_negY_addY`).
 We only need to verify the base cases `n = 1` and `n = 2`, and the induction step is handled
 by fancy identities of division polynomials and elliptic divisibility sequences
 (`smulX_sub_sub_smulX_add`, `smulX_add` and `smulY_add_sub_negY`).
@@ -72,7 +72,7 @@ instead of `Frac(Universal.Ring) = Frac(ℤ[A₁,A₂,A₃,A₄,A₆,X,Y]/⟨P
 result by specializing the characteristic 0, universal result.
 -/
 
-open scoped PolynomialPolynomial
+open scoped Polynomial.Bivariate
 
 namespace WeierstrassCurve
 
@@ -323,7 +323,7 @@ theorem zsmul_point_eq_smulX_smulY : n ≠ 0 →
     obtain _|_|_|n := n
     · exact (h0 rfl).elim
     · simp_rw [zero_add, Nat.cast_one, one_zsmul, smulX_one, smulY_one]
-      exact ⟨EllipticCurve.Affine.nonsingular pointedCurve equation_point, rfl⟩
+      exact ⟨equation_iff_nonsingular.mp equation_point, rfl⟩
     all_goals obtain ⟨ns, eq⟩ := ih 1 (by omega) one_ne_zero
     · erw [← addX_smul_one_smul_one, ← addY_smul_one_smul_one, zero_add, add_zsmul _ 1 1, eq]
       exact ⟨Affine.nonsingular_add ns ns fun _ ↦ smulY_one_ne_negY,
@@ -338,13 +338,13 @@ theorem zsmul_point_eq_smulX_smulY : n ≠ 0 →
     let L := _U.slope (smulX n2) (smulX 1) (smulY n2) (smulY 1)
     have X_eq : smulX (n2 + 1 : ℕ) = _U.addX (smulX n2) (smulX 1) L := by
       rw [Nat.cast_add, Nat.cast_one, smulX_add one_ne_zero (by omega) (by omega) (by omega),
-        Affine.addX_eq_subX_sub _ _ ne, sub_eq_add_neg (n2 : ℤ), ← eq1.1]; rfl
+        Affine.addX_eq_addX_negY_sub _ _ ne, sub_eq_add_neg (n2 : ℤ), ← eq1.1]; rfl
     have Y_eq : smulY (n2 + 1 : ℕ) = _U.addY (smulX n2) (smulX 1) (smulY n2) L := by
       rw [← mul_cancel_left_mem_nonZeroDivisors (mem_nonZeroDivisors_of_ne_zero Field.two_ne_zero),
         ← add_right_cancel_iff (a := _U.a₁ * smulX (n2 + 1 : ℕ) + _U.a₃)]
       convert smulY_add_sub_negY (n := n2) one_ne_zero (by omega) (by omega) (by omega) using 1
       · simp_rw [Affine.negY, Nat.cast_add]; ring_nf
-      convert _U.addY_sub_negY (smulY n2) (smulY 1) ne using 1
+      convert _U.addY_sub_negY_addY (smulY n2) (smulY 1) ne using 1
       · rw [Affine.negY, ← X_eq]; ring
       · rw [← X_eq]; rfl
     rw [X_eq, Y_eq, n2.cast_add, add_zsmul, eq, eq2]

Mathlib/AlgebraicGeometry/EllipticCurve/Universal.lean

@@ -3,7 +3,7 @@ Copyright (c) 2024 Junyan Xu. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Junyan Xu
 -/
-import Mathlib.AlgebraicGeometry.EllipticCurve.Group
+import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
 
 /-!
 # The universal elliptic curve
@@ -27,7 +27,7 @@ order on the universal pointed elliptic curve.
 
 noncomputable section
 
-open scoped PolynomialPolynomial
+open scoped Polynomial.Bivariate
 
 namespace WeierstrassCurve
 
@@ -37,7 +37,7 @@ inductive Coeff : Type | A₁ : Coeff | A₂ : Coeff | A₃ : Coeff | A₄ : Coe
 
 namespace Universal
 
-open scoped Polynomial PolynomialPolynomial
+open scoped Polynomial Polynomial.Bivariate
 open Coeff
 
 open MvPolynomial (X) in
@@ -86,26 +86,33 @@ lemma algebraMap_ring_eq_comp :
 lemma algebraMap_field_injective :
     Function.Injective (algebraMap (MvPolynomial Coeff ℤ) Universal.Field) :=
   (IsFractionRing.injective Universal.Ring Universal.Field).comp
-    (Affine.CoordinateRing.algebraMap_injective' _)
+    (Affine.CoordinateRing.algebraMap_injective' (W' := curve))
 
 /-- The universal pointed Weierstrass curve is an elliptic curve
-when base-changed to the the universal field. -/
-def pointedCurve : EllipticCurve Universal.Field where
-  __ := baseChange curve Universal.Field
-  Δ' := .mk0 (baseChange curve Universal.Field).Δ <| by
-    simpa only [map_Δ, map_ne_zero_iff _ algebraMap_field_injective] using Δ_curve_ne_zero
-  coe_Δ' := rfl
+when base-changed to the universal field. -/
+abbrev pointedCurve : WeierstrassCurve Universal.Field := baseChange curve Universal.Field
+
+instance : pointedCurve.IsElliptic where
+  isUnit := by
+    rw [show pointedCurve.Δ = _ from map_Δ curve (algebraMap _ Universal.Field)]
+    exact ((map_ne_zero_iff _ algebraMap_field_injective).mpr Δ_curve_ne_zero).isUnit
 
 open Polynomial in
 lemma equation_point : pointedCurve.toAffine.Equation (polyToField (C X)) (polyToField Y) := by
-  simp_rw [Affine.Equation, pointedCurve, baseChange, EllipticCurve.toAffine,
-    algebraMap_field_eq_comp, ← map_map, Affine.map_polynomial_evalEval, Affine.map_polynomial,
-    evalEval, eval_map, eval_C_X_eval₂_map_C_X, polyToField_polynomial]
+  show evalEval (polyToField (C X)) (polyToField Y)
+    ((curve.map (algebraMap _ Universal.Field)).toAffine.polynomial) = 0
+  have h : (evalEvalRingHom (polyToField (C X)) (polyToField Y)).comp
+      (mapRingHom <| mapRingHom (algebraMap _ Universal.Field)) = polyToField := by
+    ext <;> simp [polyToField, algebraMap_field_eq_comp]
+  have : ∀ p, evalEval (polyToField (C X)) (polyToField Y)
+      (p.map (mapRingHom (algebraMap _ Universal.Field))) = polyToField p :=
+    fun p ↦ congr($h p)
+  rw [Affine.map_polynomial, this, polyToField_polynomial]
 
 open Polynomial Affine in
 /-- The distinguished point on the universal pointed Weierstrass curve. -/
 def Affine.point : curve⟮Universal.Field⟯ :=
-  .some (EllipticCurve.Affine.nonsingular pointedCurve equation_point)
+  .some (equation_iff_nonsingular.mp equation_point)
 
 /-- The distinguished point on the universal curve in Jacobian coordinates. -/
 def Jacobian.point : Jacobian.Point (curve.baseChange Universal.Field) :=
@@ -128,7 +135,7 @@ abbrev curveRing : WeierstrassCurve Universal.Ring := curve.baseChange Universal
 (the universal field), where `P` is the Weierstrass polynomial. -/
 abbrev curveField : WeierstrassCurve Universal.Field := curve.baseChange Universal.Field
 
-lemma curveField_eq : curveField = pointedCurve.toWeierstrassCurve := rfl
+lemma curveField_eq : curveField = pointedCurve := rfl
 
 end Universal
 
@@ -190,8 +197,9 @@ protected lemma Field.two_ne_zero : (2 : Universal.Field) ≠ 0 := by
   intro h; replace h := congr(ringEval cusp_equation_one_one $h)
   rw [map_ofNat, map_zero] at h; cases h
 
-lemma curveRing_map_ringEval : curveRing.map (ringEval eqn) = W := by
-  rw [curveRing, baseChange, map_map, ringEval_comp_eq_specialize, map_specialize]
+lemma curveRing_map_ringEval : curveRing.map (ringEval eqn) = W :=
+  (map_map curve (algebraMap _ _) (ringEval eqn)).symm ▸
+    (ringEval_comp_eq_specialize eqn) ▸ map_specialize W
 
 end Universal