[Merged by Bors] - feat(AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic): add maps for division polynomials

Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean

@@ -10,13 +10,13 @@ import Mathlib.NumberTheory.EllipticDivisibilitySequence
 # Division polynomials of Weierstrass curves
 
 This file defines certain polynomials associated to division polynomials of Weierstrass curves.
-These are defined in terms of the auxiliary sequences of normalised elliptic divisibility sequences
-defined in `Mathlib.NumberTheory.EllipticDivisibilitySequence`.
+These are defined in terms of the auxiliary sequences for normalised elliptic divisibility sequences
+(EDS) as defined in `Mathlib.NumberTheory.EllipticDivisibilitySequence`.
 
 ## Mathematical background
 
 Let $W$ be a Weierstrass curve over a commutative ring $R$. The sequence of $n$-division polynomials
-$\psi_n \in R[X, Y]$ of $W$ is the normalised elliptic divisibility sequence with initial values
+$\psi_n \in R[X, Y]$ of $W$ is the normalised EDS with initial values
  * $\psi_0 := 0$,
  * $\psi_1 := 1$,
  * $\psi_2 := 2Y + a_1X + a_3$,
@@ -28,8 +28,8 @@ Furthermore, define the associated sequences $\phi_n, \omega_n \in R[X, Y]$ by
  * $\phi_n := X\psi_n^2 - \psi_{n + 1}\psi_{n - 1}$, and
  * $\omega_n := \tfrac{1}{2} \cdot (\psi_{2n} / \psi_n - \psi_n(a_1\phi_n + a_3\psi_n^2))$.
 
-Note that $\omega_n$ is always well-defined as a polynomial. As a start, it can be shown by
-induction that $\psi_n$ always divides $\psi_{2n}$, so that $\psi_{2n} / \psi_n$ is always
+Note that $\omega_n$ is always well-defined as a polynomial in $R[X, Y]$. As a start, it can be
+shown by induction that $\psi_n$ always divides $\psi_{2n}$, so that $\psi_{2n} / \psi_n$ is always
 well-defined as a polynomial, while division by 2 is well-defined when $R$ has characteristic
 different from 2. In general, it can be shown that 2 always divides the polynomial
 $\psi_{2n} / \psi_n - \psi_n(a_1\phi_n + a_3\psi_n^2)$ in the characteristic zero universal ring
@@ -38,16 +38,16 @@ defined as its image under the associated universal morphism $\mathbb{Z}[A_i][X,
 
 Now, in the coordinate ring $R[W]$, note that $\psi_2^2$ is congruent to the polynomial
 $\Psi_2^{[2]} := 4X^3 + b_2X^2 + 2b_4X + b_6 \in R[X]$. As such, in $R[W]$, the recurrences
-associated to a normalised elliptic divisibility sequence show that $\psi_n / \psi_2$ are congruent
-to certain polynomials in $R[X]$. In particular, define $\tilde{\Psi}_n \in R[X]$ as the auxiliary
-sequence for a normalised elliptic divisibility sequence with initial values
+associated to a normalised EDS show that $\psi_n / \psi_2$ are congruent to certain polynomials in
+$R[X]$. In particular, define $\tilde{\Psi}_n \in R[X]$ as the auxiliary sequence for a normalised
+EDS with extraneous parameter $\Psi_2^{[2]}$ and initial values
  * $\tilde{\Psi}_0 := 0$,
  * $\tilde{\Psi}_1 := 1$,
  * $\tilde{\Psi}_2 := 1$,
  * $\tilde{\Psi}_3 := \psi_3$, and
  * $\tilde{\Psi}_4 := \psi_4 / \psi_2$.
 
-The corresponding normalised elliptic divisibility sequence $\Psi_n \in R[X, Y]$ is then given by
+The corresponding normalised EDS $\Psi_n \in R[X, Y]$ is then given by
  * $\Psi_n := \tilde{\Psi}_n\psi_2$ if $n$ is even, and
  * $\Psi_n := \tilde{\Psi}_n$ if $n$ is odd.
 

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

@@ -42,10 +42,10 @@ Some examples of EDSs include
 ## Implementation notes
 
 The normalised EDS `normEDS b c d n` is defined in terms of the auxiliary sequence
-`preNormEDS (b ^ 4) c d n`, which are equal when `n` is odd, and which differ by a factor of `b`
-when `n` is even. This coincides with the definition in the references since both agree for
-`normEDS b c d 2` and for `normEDS b c d 4`, and the correct factors of `b` are removed in
-`normEDS b c d (2 * (m + 2) + 1)` and in `normEDS b c d (2 * (m + 3))`.
+`preNormEDS (b ^ 4) c d n`, which are equal when `n` is odd, and which differ by a factor of an
+extraneous parameter `b` when `n` is even. This coincides with the definition in the references
+since both agree for `normEDS b c d 2` and for `normEDS b c d 4`, and the correct factors of `b` are
+removed in `normEDS b c d (2 * (m + 2) + 1)` and in `normEDS b c d (2 * (m + 3))`.
 
 One reason is to avoid the necessity for ring division by `b` in the inductive definition of
 `normEDS b c d (2 * (m + 3))`. The idea is that, it can be shown that `normEDS b c d (2 * (m + 3))`
@@ -102,8 +102,8 @@ lemma IsDivSequence.smul (h : IsDivSequence W) (x : R) : IsDivSequence (x • W)
 lemma IsEllDivSequence.smul (h : IsEllDivSequence W) (x : R) : IsEllDivSequence (x • W) :=
   ⟨h.left.smul x, h.right.smul x⟩
 
-/-- The auxiliary sequence for a normalised EDS `W : ℕ → R`,
-with initial values `W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d`. -/
+/-- The auxiliary sequence for a normalised EDS `W : ℕ → R`, with extraneous parameter `b` and
+initial values `W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d`. -/
 def preNormEDS' (b c d : R) : ℕ → R
   | 0 => 0
   | 1 => 1
@@ -159,8 +159,8 @@ lemma preNormEDS'_even (m : ℕ) : preNormEDS' b c d (2 * (m + 3)) =
   simp only [Nat.mul_add_div two_pos]
   rfl
 
-/-- The auxiliary sequence for a normalised EDS `W : ℤ → R`,
-with initial values `W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d`.
+/-- The auxiliary sequence for a normalised EDS `W : ℤ → R`, with extraneous parameter `b` and
+initial values `W(0) = 0`, `W(1) = 1`, `W(2) = 1`, `W(3) = c`, and `W(4) = d`.
 
 This extends `preNormEDS'` by defining its values at negative integers. -/
 def preNormEDS (n : ℤ) : R :=
@@ -208,8 +208,8 @@ lemma preNormEDS_even (m : ℕ) : preNormEDS b c d (2 * (m + 3)) =
 lemma preNormEDS_neg (n : ℤ) : preNormEDS b c d (-n) = -preNormEDS b c d n := by
   rw [preNormEDS, Int.sign_neg, Int.cast_neg, neg_mul, Int.natAbs_neg, preNormEDS]
 
-/-- The canonical example of a normalised EDS `W : ℤ → R`,
-with initial values `W(0) = 0`, `W(1) = 1`, `W(2) = b`, `W(3) = c`, and `W(4) = d * b`.
+/-- The canonical example of a normalised EDS `W : ℤ → R`, with initial values
+`W(0) = 0`, `W(1) = 1`, `W(2) = b`, `W(3) = c`, and `W(4) = d * b`.
 
 This is defined in terms of `preNormEDS` whose even terms differ by a factor of `b`. -/
 def normEDS (n : ℤ) : R :=