Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

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 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 EDS with initial values

Furthermore, define the associated sequences $\phi_n, \omega_n \in R[X, Y]$ by

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}$ in $R[X, Y]$, 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 \cdot (a_1\phi_n + a_3\psi_n^2)$ in the characteristic zero universal ring $\mathcal{R}[X, Y] := \mathbb{Z}[A_1, A_2, A_3, A_4, A_6][X, Y]$ of $W$, where the $A_i$ are indeterminates. Then $\omega_n$ can be equivalently defined as the image of this division under the associated universal morphism $\mathcal{R}[X, Y] \to R[X, Y]$ mapping $A_i$ to $a_i$.

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 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 extra parameter $(\Psi_2^{[2]})^2$ and initial values

The corresponding normalised EDS $\Psi_n \in R[X, Y]$ is then given by

Furthermore, define the associated sequences $\Psi_n^{[2]}, \Phi_n \in R[X]$ by

With these definitions in mind, $\psi_n \in R[X, Y]$ and $\phi_n \in R[X, Y]$ are congruent in $R[W]$ to $\Psi_n \in R[X, Y]$ and $\Phi_n \in R[X]$ respectively, which are defined in terms of $\Psi_2^{[2]} \in R[X]$ and $\tilde{\Psi}_n \in R[X]$.

Main definitions #

Implementation notes #

Analogously to Mathlib.NumberTheory.EllipticDivisibilitySequence, the bivariate polynomials $\Psi_n$ are defined in terms of the univariate polynomials $\tilde{\Psi}_n$. This is done partially to avoid ring division, but more crucially to allow the definition of $\Psi_n^{[2]}$ and $\Phi_n$ as univariate polynomials without needing to work under the coordinate ring, and to allow the computation of their leading terms without ambiguity. Furthermore, evaluating these polynomials at a rational point on $W$ recovers their original definition up to linear combinations of the Weierstrass equation of $W$, hence also avoiding the need to work in the coordinate ring.

TODO: implementation notes for the definition of $\omega_n$.

References #

[J Silverman, The Arithmetic of Elliptic Curves][silverman2009]

Tags #

elliptic curve, division polynomial, torsion point

The univariate polynomial $\Psi_2^{[2]}$ #

noncomputable def WeierstrassCurve.ψ₂ {R : Type r} [CommRing R] (W : WeierstrassCurve R) :

The $2$-division polynomial $\psi_2 = \Psi_2$.

Equations
  • W.ψ₂ = W.toAffine.polynomialY
Instances For
    noncomputable def WeierstrassCurve.Ψ₂Sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) :

    The univariate polynomial $\Psi_2^{[2]}$ congruent to $\psi_2^2$.

    Equations
    • W.Ψ₂Sq = Polynomial.C 4 * Polynomial.X ^ 3 + Polynomial.C W.b₂ * Polynomial.X ^ 2 + Polynomial.C (2 * W.b₄) * Polynomial.X + Polynomial.C W.b₆
    Instances For
      theorem WeierstrassCurve.C_Ψ₂Sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
      Polynomial.C W.Ψ₂Sq = W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial
      theorem WeierstrassCurve.ψ₂_sq {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
      W.ψ₂ ^ 2 = Polynomial.C W.Ψ₂Sq + 4 * W.toAffine.polynomial
      theorem WeierstrassCurve.Ψ₂Sq_eq {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
      W.Ψ₂Sq = W.twoTorsionPolynomial.toPoly

      The univariate polynomials $\tilde{\Psi}_n$ for $n \in \mathbb{N}$ #

      noncomputable def WeierstrassCurve.Ψ₃ {R : Type r} [CommRing R] (W : WeierstrassCurve R) :

      The $3$-division polynomial $\psi_3 = \Psi_3$.

      Equations
      • W.Ψ₃ = 3 * Polynomial.X ^ 4 + Polynomial.C W.b₂ * Polynomial.X ^ 3 + 3 * Polynomial.C W.b₄ * Polynomial.X ^ 2 + 3 * Polynomial.C W.b₆ * Polynomial.X + Polynomial.C W.b₈
      Instances For
        noncomputable def WeierstrassCurve.preΨ₄ {R : Type r} [CommRing R] (W : WeierstrassCurve R) :

        The univariate polynomial $\tilde{\Psi}_4$, which is auxiliary to the $4$-division polynomial $\psi_4 = \Psi_4 = \tilde{\Psi}_4\psi_2$.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          noncomputable def WeierstrassCurve.preΨ' {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

          The univariate polynomials $\tilde{\Psi}_n$ for $n \in \mathbb{N}$, which are auxiliary to the bivariate polynomials $\Psi_n$ congruent to the bivariate $n$-division polynomials $\psi_n$.

          Equations
          Instances For
            @[simp]
            theorem WeierstrassCurve.preΨ'_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
            W.preΨ' 0 = 0
            @[simp]
            theorem WeierstrassCurve.preΨ'_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
            W.preΨ' 1 = 1
            @[simp]
            theorem WeierstrassCurve.preΨ'_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
            W.preΨ' 2 = 1
            @[simp]
            theorem WeierstrassCurve.preΨ'_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
            W.preΨ' 3 = W.Ψ₃
            @[simp]
            theorem WeierstrassCurve.preΨ'_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
            W.preΨ' 4 = W.preΨ₄
            theorem WeierstrassCurve.preΨ'_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
            W.preΨ' (2 * (m + 2) + 1) = (W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2
            theorem WeierstrassCurve.preΨ'_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
            W.preΨ' (2 * (m + 3)) = W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2

            The univariate polynomials $\tilde{\Psi}_n$ for $n \in \mathbb{Z}$ #

            noncomputable def WeierstrassCurve.preΨ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

            The univariate polynomials $\tilde{\Psi}_n$ for $n \in \mathbb{Z}$, which are auxiliary to the bivariate polynomials $\Psi_n$ congruent to the bivariate $n$-division polynomials $\psi_n$.

            Equations
            Instances For
              @[simp]
              theorem WeierstrassCurve.preΨ_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
              W.preΨ n = W.preΨ' n
              @[simp]
              theorem WeierstrassCurve.preΨ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
              W.preΨ 0 = 0
              @[simp]
              theorem WeierstrassCurve.preΨ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
              W.preΨ 1 = 1
              @[simp]
              theorem WeierstrassCurve.preΨ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
              W.preΨ 2 = 1
              @[simp]
              theorem WeierstrassCurve.preΨ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
              W.preΨ 3 = W.Ψ₃
              @[simp]
              theorem WeierstrassCurve.preΨ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
              W.preΨ 4 = W.preΨ₄
              theorem WeierstrassCurve.preΨ_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
              W.preΨ (2 * (m + 2) + 1) = (W.preΨ (m + 4) * W.preΨ (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ (m + 1) * W.preΨ (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2
              theorem WeierstrassCurve.preΨ_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
              W.preΨ (2 * (m + 3)) = W.preΨ (m + 2) ^ 2 * W.preΨ (m + 3) * W.preΨ (m + 5) - W.preΨ (m + 1) * W.preΨ (m + 3) * W.preΨ (m + 4) ^ 2
              @[simp]
              theorem WeierstrassCurve.preΨ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
              W.preΨ (-n) = -W.preΨ n

              The univariate polynomials $\Psi_n^{[2]}$ #

              noncomputable def WeierstrassCurve.ΨSq {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

              The univariate polynomials $\Psi_n^{[2]}$ congruent to $\psi_n^2$.

              Equations
              • W.ΨSq n = W.preΨ n ^ 2 * if Even n then W.Ψ₂Sq else 1
              Instances For
                @[simp]
                theorem WeierstrassCurve.ΨSq_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                W.ΨSq n = W.preΨ' n ^ 2 * if Even n then W.Ψ₂Sq else 1
                @[simp]
                theorem WeierstrassCurve.ΨSq_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                W.ΨSq 0 = 0
                @[simp]
                theorem WeierstrassCurve.ΨSq_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                W.ΨSq 1 = 1
                @[simp]
                theorem WeierstrassCurve.ΨSq_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                W.ΨSq 2 = W.Ψ₂Sq
                @[simp]
                theorem WeierstrassCurve.ΨSq_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                W.ΨSq 3 = W.Ψ₃ ^ 2
                @[simp]
                theorem WeierstrassCurve.ΨSq_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                W.ΨSq 4 = W.preΨ₄ ^ 2 * W.Ψ₂Sq
                theorem WeierstrassCurve.ΨSq_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
                W.ΨSq (2 * (m + 2) + 1) = ((W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) - W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^ 2
                theorem WeierstrassCurve.ΨSq_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
                W.ΨSq (2 * (m + 3)) = (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq
                @[simp]
                theorem WeierstrassCurve.ΨSq_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                W.ΨSq (-n) = W.ΨSq n

                The bivariate polynomials $\Psi_n$ #

                noncomputable def WeierstrassCurve.Ψ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

                The bivariate polynomials $\Psi_n$ congruent to the $n$-division polynomials $\psi_n$.

                Equations
                • W n = Polynomial.C (W.preΨ n) * if Even n then W.ψ₂ else 1
                Instances For
                  @[simp]
                  theorem WeierstrassCurve.Ψ_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                  W n = Polynomial.C (W.preΨ' n) * if Even n then W.ψ₂ else 1
                  @[simp]
                  theorem WeierstrassCurve.Ψ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                  W 0 = 0
                  @[simp]
                  theorem WeierstrassCurve.Ψ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                  W 1 = 1
                  @[simp]
                  theorem WeierstrassCurve.Ψ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                  W 2 = W.ψ₂
                  @[simp]
                  theorem WeierstrassCurve.Ψ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                  W 3 = Polynomial.C W.Ψ₃
                  @[simp]
                  theorem WeierstrassCurve.Ψ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                  W 4 = Polynomial.C W.preΨ₄ * W.ψ₂
                  theorem WeierstrassCurve.Ψ_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
                  W (2 * (m + 2) + 1) = W (m + 4) * W (m + 2) ^ 3 - W (m + 1) * W (m + 3) ^ 3 + W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * Polynomial.C (if Even m then W.preΨ' (m + 4) * W.preΨ' (m + 2) ^ 3 else -W.preΨ' (m + 1) * W.preΨ' (m + 3) ^ 3)
                  theorem WeierstrassCurve.Ψ_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
                  W (2 * (m + 3)) * W.ψ₂ = W (m + 2) ^ 2 * W (m + 3) * W (m + 5) - W (m + 1) * W (m + 3) * W (m + 4) ^ 2
                  @[simp]
                  theorem WeierstrassCurve.Ψ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                  W (-n) = -W n

                  The univariate polynomials $\Phi_n$ #

                  noncomputable def WeierstrassCurve.Φ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

                  The univariate polynomials $\Phi_n$ congruent to $\phi_n$.

                  Equations
                  • W n = Polynomial.X * W.ΨSq n - W.preΨ (n + 1) * W.preΨ (n - 1) * if Even n then 1 else W.Ψ₂Sq
                  Instances For
                    @[simp]
                    theorem WeierstrassCurve.Φ_ofNat {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                    W (n + 1) = (Polynomial.X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) - W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
                    @[simp]
                    theorem WeierstrassCurve.Φ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                    W 0 = 1
                    @[simp]
                    theorem WeierstrassCurve.Φ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                    W 1 = Polynomial.X
                    @[simp]
                    theorem WeierstrassCurve.Φ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                    W 2 = Polynomial.X ^ 4 - Polynomial.C W.b₄ * Polynomial.X ^ 2 - Polynomial.C (2 * W.b₆) * Polynomial.X - Polynomial.C W.b₈
                    @[simp]
                    theorem WeierstrassCurve.Φ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                    W 3 = Polynomial.X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq
                    @[simp]
                    theorem WeierstrassCurve.Φ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                    W 4 = Polynomial.X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
                    @[simp]
                    theorem WeierstrassCurve.Φ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                    W (-n) = W n

                    The bivariate polynomials $\psi_n$ #

                    noncomputable def WeierstrassCurve.ψ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

                    The bivariate $n$-division polynomials $\psi_n$.

                    Equations
                    • W n = normEDS W.ψ₂ (Polynomial.C W.Ψ₃) (Polynomial.C W.preΨ₄) n
                    Instances For
                      @[simp]
                      theorem WeierstrassCurve.ψ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                      W 0 = 0
                      @[simp]
                      theorem WeierstrassCurve.ψ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                      W 1 = 1
                      @[simp]
                      theorem WeierstrassCurve.ψ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                      W 2 = W.ψ₂
                      @[simp]
                      theorem WeierstrassCurve.ψ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                      W 3 = Polynomial.C W.Ψ₃
                      @[simp]
                      theorem WeierstrassCurve.ψ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                      W 4 = Polynomial.C W.preΨ₄ * W.ψ₂
                      theorem WeierstrassCurve.ψ_odd {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
                      W (2 * (m + 2) + 1) = W (m + 4) * W (m + 2) ^ 3 - W (m + 1) * W (m + 3) ^ 3
                      theorem WeierstrassCurve.ψ_even {R : Type r} [CommRing R] (W : WeierstrassCurve R) (m : ) :
                      W (2 * (m + 3)) * W.ψ₂ = W (m + 2) ^ 2 * W (m + 3) * W (m + 5) - W (m + 1) * W (m + 3) * W (m + 4) ^ 2
                      @[simp]
                      theorem WeierstrassCurve.ψ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                      W (-n) = -W n

                      The bivariate polynomials $\phi_n$ #

                      noncomputable def WeierstrassCurve.φ {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :

                      The bivariate polynomials $\phi_n$.

                      Equations
                      • W n = Polynomial.C Polynomial.X * W n ^ 2 - W (n + 1) * W (n - 1)
                      Instances For
                        @[simp]
                        theorem WeierstrassCurve.φ_zero {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                        W 0 = 1
                        @[simp]
                        theorem WeierstrassCurve.φ_one {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                        W 1 = Polynomial.C Polynomial.X
                        @[simp]
                        theorem WeierstrassCurve.φ_two {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                        W 2 = Polynomial.C Polynomial.X * W.ψ₂ ^ 2 - Polynomial.C W.Ψ₃
                        @[simp]
                        theorem WeierstrassCurve.φ_three {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                        W 3 = Polynomial.C Polynomial.X * Polynomial.C W.Ψ₃ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 2
                        @[simp]
                        theorem WeierstrassCurve.φ_four {R : Type r} [CommRing R] (W : WeierstrassCurve R) :
                        W 4 = Polynomial.C Polynomial.X * Polynomial.C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - Polynomial.C W.preΨ₄ * W.ψ₂ ^ 4 * Polynomial.C W.Ψ₃ + Polynomial.C W.Ψ₃ ^ 4
                        @[simp]
                        theorem WeierstrassCurve.φ_neg {R : Type r} [CommRing R] (W : WeierstrassCurve R) (n : ) :
                        W (-n) = W n

                        Maps across ring homomorphisms #

                        theorem WeierstrassCurve.map_ψ₂ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) :
                        (W.map f).ψ₂ = Polynomial.map (Polynomial.mapRingHom f) W.ψ₂
                        theorem WeierstrassCurve.map_Ψ₂Sq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) :
                        (W.map f).Ψ₂Sq = Polynomial.map f W.Ψ₂Sq
                        theorem WeierstrassCurve.map_Ψ₃ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) :
                        (W.map f).Ψ₃ = Polynomial.map f W.Ψ₃
                        theorem WeierstrassCurve.map_preΨ₄ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) :
                        (W.map f).preΨ₄ = Polynomial.map f W.preΨ₄
                        theorem WeierstrassCurve.map_preΨ' {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f).preΨ' n = Polynomial.map f (W.preΨ' n)
                        theorem WeierstrassCurve.map_preΨ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f).preΨ n = Polynomial.map f (W.preΨ n)
                        theorem WeierstrassCurve.map_ΨSq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f).ΨSq n = Polynomial.map f (W.ΨSq n)
                        theorem WeierstrassCurve.map_Ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f) n = Polynomial.map (Polynomial.mapRingHom f) (W n)
                        theorem WeierstrassCurve.map_Φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f) n = Polynomial.map f (W n)
                        theorem WeierstrassCurve.map_ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f) n = Polynomial.map (Polynomial.mapRingHom f) (W n)
                        theorem WeierstrassCurve.map_φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ) :
                        (W.map f) n = Polynomial.map (Polynomial.mapRingHom f) (W n)

                        Base changes across algebra homomorphisms #

                        theorem WeierstrassCurve.baseChange_ψ₂ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                        (W.baseChange B).ψ₂ = Polynomial.map (Polynomial.mapRingHom f) (W.baseChange A).ψ₂
                        theorem WeierstrassCurve.baseChange_Ψ₂Sq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                        (W.baseChange B).Ψ₂Sq = Polynomial.map (↑f) (W.baseChange A).Ψ₂Sq
                        theorem WeierstrassCurve.baseChange_Ψ₃ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                        (W.baseChange B).Ψ₃ = Polynomial.map (↑f) (W.baseChange A).Ψ₃
                        theorem WeierstrassCurve.baseChange_preΨ₄ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) :
                        (W.baseChange B).preΨ₄ = Polynomial.map (↑f) (W.baseChange A).preΨ₄
                        theorem WeierstrassCurve.baseChange_preΨ' {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B).preΨ' n = Polynomial.map (↑f) ((W.baseChange A).preΨ' n)
                        theorem WeierstrassCurve.baseChange_preΨ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B).preΨ n = Polynomial.map (↑f) ((W.baseChange A).preΨ n)
                        theorem WeierstrassCurve.baseChange_ΨSq {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B).ΨSq n = Polynomial.map (↑f) ((W.baseChange A).ΨSq n)
                        theorem WeierstrassCurve.baseChange_Ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B) n = Polynomial.map (Polynomial.mapRingHom f) ((W.baseChange A) n)
                        theorem WeierstrassCurve.baseChange_Φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B) n = Polynomial.map (↑f) ((W.baseChange A) n)
                        theorem WeierstrassCurve.baseChange_ψ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B) n = Polynomial.map (Polynomial.mapRingHom f) ((W.baseChange A) n)
                        theorem WeierstrassCurve.baseChange_φ {R : Type r} {S : Type s} [CommRing R] [CommRing S] (W : WeierstrassCurve R) [Algebra R S] {A : Type u} [CommRing A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] {B : Type v} [CommRing B] [Algebra R B] [Algebra S B] [IsScalarTower R S B] (f : A →ₐ[S] B) (n : ) :
                        (W.baseChange B) n = Polynomial.map (Polynomial.mapRingHom f) ((W.baseChange A) n)