feat(EllipticCurve): ZSMul formula in terms of division polynomials

Mathlib.lean

@@ -589,6 +589,7 @@ import Mathlib.Algebra.Pointwise.Stabilizer
 import Mathlib.Algebra.Polynomial.AlgebraMap
 import Mathlib.Algebra.Polynomial.Basic
 import Mathlib.Algebra.Polynomial.BigOperators
+import Mathlib.Algebra.Polynomial.Bivariate
 import Mathlib.Algebra.Polynomial.CancelLeads
 import Mathlib.Algebra.Polynomial.Cardinal
 import Mathlib.Algebra.Polynomial.Coeff
@@ -706,9 +707,11 @@ import Mathlib.Algebra.Vertex.HVertexOperator
 import Mathlib.AlgebraicGeometry.AffineScheme
 import Mathlib.AlgebraicGeometry.EllipticCurve.Affine
 import Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
+import Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.ZSMul
 import Mathlib.AlgebraicGeometry.EllipticCurve.Group
 import Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian
 import Mathlib.AlgebraicGeometry.EllipticCurve.Projective
+import Mathlib.AlgebraicGeometry.EllipticCurve.Universal
 import Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
 import Mathlib.AlgebraicGeometry.FunctionField
 import Mathlib.AlgebraicGeometry.GammaSpecAdjunction

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/Algebra/Polynomial/Bivariate.lean

@@ -0,0 +1,73 @@
+/-
+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.Algebra.Polynomial.AlgebraMap
+
+/-!
+# Bivariate polynomials
+
+This file introduces the notation `R[X][Y]` for the polynomial ring `R[X][X]` in two variables,
+and the notation `Y` for the second variable, in the `PolynomialPolynomial` scope.
+
+It also defines `Polynomial.evalEval` for the evaluation of a bivariate polynomial at a point
+on the affine plane, which is a ring homomorphism (`Polynomial.evalEvalRingHom`), as well as
+the abbreviation `CC` to view a constant in the base ring `R` as a bivariate polynomial.
+-/
+
+/-- The notation `Y` for `X` in the `PolynomialPolynomial` scope. -/
+scoped[PolynomialPolynomial] notation3:max "Y" => Polynomial.X (R := Polynomial _)
+
+/-- The notation `R[X][Y]` for `R[X][X]` in the `PolynomialPolynomial` scope. -/
+scoped[PolynomialPolynomial] notation3:max R "[X][Y]" => Polynomial (Polynomial R)
+
+namespace Polynomial
+
+noncomputable section
+
+open scoped PolynomialPolynomial
+
+variable {R : Type*}
+
+/-- `evalEval x y p` is the evaluation `p(x,y)` of a two-variable polynomial `p : R[X][Y]`. -/
+abbrev evalEval [Semiring R] (x y : R) (p : R[X][Y]) : R := eval x (eval (C y) p)
+
+/-- `evalEval x y` as a ring homomorphism. -/
+@[simps!] abbrev evalEvalRingHom [CommSemiring R] (x y : R) : R[X][Y] →+* R :=
+  (evalRingHom x).comp (evalRingHom <| C y)
+
+/-- A constant viewed as a polynomial in two variables. -/
+abbrev CC [Semiring R] (r : R) : R[X][Y] := C (C r)
+
+lemma coe_algebraMap_eq_CC [CommSemiring R] : algebraMap R R[X][Y] = CC (R := R) := rfl
+lemma coe_evalEvalRingHom [CommSemiring R] (x y : R) : evalEvalRingHom x y = evalEval x y := rfl
+
+variable {S} [CommSemiring R] [CommSemiring S]
+
+/-- Two equivalent ways to express the evaluation of a bivariate polynomial over `R`
+at a point in the affine plane over an `R`-algebra `S`. -/
+lemma eval₂RingHom_eval₂RingHom (f : R →+* S) (x y : S) :
+    eval₂RingHom (eval₂RingHom f x) y =
+      (evalEvalRingHom x y).comp (mapRingHom <| mapRingHom f) := by
+  ext <;> simp
+
+lemma eval₂_eval₂RingHom_apply (f : R →+* S) (x y : S) (p : R[X][Y]) :
+    eval₂ (eval₂RingHom f x) y p = (p.map <| mapRingHom f).evalEval x y :=
+  congr($(eval₂RingHom_eval₂RingHom f x y) p)
+
+lemma eval_C_X_comp_eval₂_map_C_X :
+    (evalRingHom (C X : R[X][Y])).comp (eval₂RingHom (mapRingHom <| algebraMap R R[X][Y]) (C Y)) =
+      .id _ := by
+  ext <;> simp
+
+/-- Since `R[X,Y,X']` is an `R[X']`-algebra, a polynomial `p : R[X',Y']` can be evaluated at
+`Y : R[X,Y,X']` (substitution of `Y'` by `Y`), obtaining another polynomial in `R[X,Y,X']`.
+When this polynomial is then evaluated at `X' = X`, the original polynomial `p` is recovered. -/
+lemma eval_C_X_eval₂_map_C_X {p : R[X][Y]} :
+    eval (C X) (eval₂ (mapRingHom <| algebraMap R R[X][Y]) (C Y) p) = p :=
+  congr($eval_C_X_comp_eval₂_map_C_X p)
+
+end
+
+end Polynomial