Elliptic divisibility sequences, universal Weierstrass curve, division polynomial ω

Definition: WeierstrassCurve_EDSEngine (5fd20a59-e5e9-5133-a421-34f512baf1be), by Claude, 2026-09-05.

Four layers are set up here. (1) Sequence identities. For $W:\mathbb{Z}\to R$ over a commutative ring, EllSequence.addMulSub W m n $= W((m+n)\,\mathrm{tdiv}\,2)\cdot W((m-n)\,\mathrm{tdiv}\,2)$, and rel₄, rel₆, relFin4, net are the associated quadratic and quartic expressions, net W p q r s $= W(p+q+s)W(p-q)W(r+s)W(r)-W(p+r+s)W(p-r)W(q+s)W(q)+W(q+r+s)W(q-r)W(p+s)W(p)$; Rel₃ W m n r is the three‑term elliptic relation at $(m,n,r)$, so that IsEllipticSequence is equivalent to $\forall m,n,r$, Rel₃. OddRec/EvenRec are the doubling recursions $W(2m+1)W(1)^3=W(m+2)W(m)^3-W(m-1)W(m+1)^3$ and $W(2m)W(2)W(1)^2=W(m)(W(m-1)^2W(m+2)-W(m-2)W(m+1)^2)$; invarNum, invarDenom form the quotient shown to be independent of $n$. The combinatorial predicates HaveSameParity₄, StrictAnti₄ ($0\le d<c<b<a$), avg₄, dMin, cMin, Rel₄OfValid organise the descent from the two recursions to the full relation. (2) Complementary sequences: compl₂EDSAux and compl₂EDS built from preNormEDS (b^4) c d, with $\mathrm{normEDS}\cdot\mathrm{compl₂EDS}=\mathrm{normEDS}(2m)$; the recursion compl', its odd extension compl, and complEDS b c d m n with $\mathrm{normEDS}(m)\cdot\mathrm{complEDS}(m,n)=\mathrm{normEDS}(nm)$; redInvarNum, redInvarDenom (the latter by cases on $m \bmod 6$) satisfy $\mathrm{redInvarNum}=\mathrm{redInvarDenom}\cdot(d+b^4)$. Universality is obtained from Param, universalNormEDS = normEDS (X B) (X C) (X D), and the specialisation $(b,c,d)=(2,3,2)$ at which normEDS is the identity. (3) The universal curve: Coeff, Univ.curve over $\mathbb{Z}[A_1,A_2,A_3,A_4,A_6]$, its bivariate polynomial ring Poly, coordinate ring Univ.Ring, fraction field Univ.Field, the map polyToField, the generic affine and Jacobian points, the cusp $y^2=x^3$ with its point $(1,1)$, and the evaluation maps specialize, polyEval, ringEval. (4) Division polynomials: invar $=6X^2+b_2X+b_4$, ψc with $\psi_n\psi^c_n=\psi_{2n}$, and ωe $n$, characterised by $2\omega_n+a_1\phi_n\psi_n+a_3\psi_n^3=\psi^c_n$, with $\omega_0=1$, $\omega_1=Y$; then smulX, smulY, slopeOne give $\phi_n/\psi_n^2$, $\omega_n/\psi_n^3$ over Univ.Field.

Relation to Mathlib. Mathlib supplies normEDS, preNormEDS and the division polynomials $\psi_n$, $\phi_n$, $\Psi_3$, $\mathrm{pre}\Psi_4$; compl₂EDS agrees with Mathlib's complEDS₂. The sequence predicates are Mathlib's IsEllipticSequence, IsDvdSequence and IsEllipticDvdSequence, with divisibility indexed by integers. The complementary sequence complEDS, the polynomial ωe, the universal Weierstrass curve with its coordinate ring and function field, and the specialisation homomorphisms have no Mathlib counterpart here.

Where it is used. The formulas assembled here express multiplication by $n$ on a Weierstrass curve through $\phi_n$, $\omega_n$ and $\psi_n$, first for the generic point of the universal curve and then, by specialisation, over an arbitrary base. They serve the treatment of torsion points of elliptic curves needed for the Galois representations attached to the Frey curve.

<!-- Generated by add_prove2me_provenance.py -->

def WeierstrassCurve.Affine.«term_⟮_⟯» : Lean.TrailingParserDescr

Notation for the affine point group after base change to the indicated coefficient ring.

Equations

• One or more equations did not get rendered due to their size.

instance WeierstrassCurve.instIsEllipticBaseChange {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (W : WeierstrassCurve R) [W.IsElliptic] : (W.baseChange A).IsElliptic

def EllSequence.addMulSub {R : Type u} [CommRing R] (W : ℤ → R) (m n : ℤ) : R

The product of sequence values at the half-sum and half-difference of the two indices.

Equations

• EllSequence.addMulSub W m n = W ((m + n).tdiv 2) * W ((m - n).tdiv 2)

def EllSequence.rel₄ {R : Type u} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : R

The three-term four-index Plücker expression formed from half-sum and half-difference products.

Equations

• One or more equations did not get rendered due to their size.

def EllSequence.net {R : Type u} [CommRing R] (W : ℤ → R) (p q r s : ℤ) : R

The four-variable elliptic-net relation expression.

Equations

• EllSequence.net W p q r s = W (p + q + s) * W (p - q) * W (r + s) * W r - W (p + r + s) * W (p - r) * W (q + s) * W q + W (q + r + s) * W (q - r) * W (p + s) * W p

theorem EllSequence.net_eq_rel₄ {R : Type u} [CommRing R] {W : ℤ → R} {p q r s : ℤ} : net W p q r s = rel₄ W (2 * p + s) (2 * q + s) (2 * r + s) s

def EllSequence.Rel₃ {R : Type u} [CommRing R] (W : ℤ → R) (m n r : ℤ) : Prop

The three-index elliptic-sequence addition relation.

Equations

• EllSequence.Rel₃ W m n r = (W (m + n) * W (m - n) * W r ^ 2 = W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2)

theorem isEllSequence_iff_rel₃ {R : Type u} [CommRing R] (W : ℤ → R) : IsEllipticSequence W ↔ ∀ (m n r : ℤ), EllSequence.Rel₃ W m n r

theorem IsEllipticSequence.rel₃ {R : Type u} [CommRing R] {W : ℤ → R} (h : IsEllipticSequence W) (m n r : ℤ) : W (m + n) * W (m - n) * W r ^ 2 = W (m + r) * W (m - r) * W n ^ 2 - W (n + r) * W (n - r) * W m ^ 2

def EllSequence.invarNum {R : Type u} [CommRing R] (W : ℤ → R) (s n : ℤ) : R

The numerator of the elliptic-sequence invariant associated to the two indices.

Equations

• EllSequence.invarNum W s n = (W (n + 2 * s) * W (n - s) ^ 2 + W (n + s) ^ 2 * W (n - 2 * s)) * W s ^ 2 + W n ^ 3 * W (2 * s) ^ 2

def EllSequence.invarDenom {R : Type u} [CommRing R] (W : ℤ → R) (s n : ℤ) : R

The denominator of the elliptic-sequence invariant associated to the two indices.

Equations

• EllSequence.invarDenom W s n = W (n + s) * W n * W (n - s)

theorem EllSequence.invar_of_net {R : Type u} [CommRing R] (W : ℤ → R) (net_eq_zero : ∀ (p q r s : ℤ), net W p q r s = 0) (s m n : ℤ) : invarNum W s m * invarDenom W s n = invarNum W s n * invarDenom W s m

theorem EllSequence.net_add_sub_iff {R : Type u} [CommRing R] (W : ℤ → R) (m n : ℤ) : net W (m + n) m (m - n) n = 0 ↔ W (2 * (m + n)) * W (m - n) * W m * W n = (W (2 * m + n) * W (2 * n) * W m - W (m + 2 * n) * W (2 * m) * W n) * W (m + n)

theorem EllSequence.addMulSub_two_zero {R : Type u} [CommRing R] (W : ℤ → R) : addMulSub W 2 0 = W 1 ^ 2

theorem EllSequence.addMulSub_three_one {R : Type u} [CommRing R] (W : ℤ → R) : addMulSub W 3 1 = W 2 * W 1

theorem EllSequence.addMulSub_even {R : Type u} [CommRing R] (W : ℤ → R) (m n : ℤ) : addMulSub W (2 * m) (2 * n) = W (m + n) * W (m - n)

theorem EllSequence.addMulSub_odd {R : Type u} [CommRing R] (W : ℤ → R) (m n : ℤ) : addMulSub W (2 * m + 1) (2 * n + 1) = W (m + n + 1) * W (m - n)

theorem EllSequence.addMulSub_same {R : Type u} [CommRing R] (W : ℤ → R) (zero : W 0 = 0) (m : ℤ) : addMulSub W m m = 0

theorem EllSequence.addMulSub_neg₀ {R : Type u} [CommRing R] (W : ℤ → R) (neg : ∀ (k : ℤ), W (-k) = -W k) (m n : ℤ) : addMulSub W (-m) n = addMulSub W m n

theorem EllSequence.addMulSub_neg₁ {R : Type u} [CommRing R] (W : ℤ → R) (m n : ℤ) : addMulSub W m (-n) = addMulSub W m n

theorem EllSequence.addMulSub_abs₀ {R : Type u} [CommRing R] (W : ℤ → R) (neg : ∀ (k : ℤ), W (-k) = -W k) (m n : ℤ) : addMulSub W |m| n = addMulSub W m n

theorem EllSequence.addMulSub_abs₁ {R : Type u} [CommRing R] (W : ℤ → R) (m n : ℤ) : addMulSub W m |n| = addMulSub W m n

theorem EllSequence.addMulSub_swap {R : Type u} [CommRing R] (W : ℤ → R) (neg : ∀ (k : ℤ), W (-k) = -W k) (m n : ℤ) : addMulSub W m n = -addMulSub W n m

def EllSequence.StrictAnti₄ (a b c d : ℤ) : Prop

The four indices are strictly decreasing and the last is nonnegative.

Equations

• EllSequence.StrictAnti₄ a b c d = (0 ≤ d ∧ d < c ∧ c < b ∧ b < a)

def EllSequence.HaveSameParity₄ (a b c d : ℤ) : Prop

The four indices have the same parity, expressed through powers of -1.

Equations

• EllSequence.HaveSameParity₄ a b c d = (a.negOnePow = b.negOnePow ∧ b.negOnePow = c.negOnePow ∧ c.negOnePow = d.negOnePow)

def EllSequence.avg₄ (a b c d : ℤ) : ℤ

Half the sum of the four indices, using integer division.

Equations

• EllSequence.avg₄ a b c d = (a + b + c + d) / 2

theorem EllSequence.HaveSameParity₄.rel₄_eq_net {R : Type u} [CommRing R] {W : ℤ → R} {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : rel₄ W a b c d = net W ((a - d) / 2) ((b - d) / 2) ((c - d) / 2) d

theorem EllSequence.HaveSameParity₄.even_sum {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : Even (a + b + c + d)

theorem EllSequence.HaveSameParity₄.avg₄_add_avg₄ {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : avg₄ a b c d + avg₄ a b c d = a + b + c + d

theorem EllSequence.HaveSameParity₄.same₀₃ {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : a.negOnePow = d.negOnePow

theorem EllSequence.HaveSameParity₄.abs {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : HaveSameParity₄ |a| |b| |c| |d|

theorem EllSequence.HaveSameParity₄.perm (σ : Equiv.Perm (Fin 4)) (t : Fin 4 → ℤ) : HaveSameParity₄ (t 0) (t 1) (t 2) (t 3) → HaveSameParity₄ (t (σ 0)) (t (σ 1)) (t (σ 2)) (t (σ 3))

theorem EllSequence.HaveSameParity₄.six_le_of_strictAnti₄ {a b c d : ℤ} (same : HaveSameParity₄ a b c d) (anti : StrictAnti₄ a b c d) : 6 ≤ a

def EllSequence.HaveSameParity₄.addMulSub₄ {R : Type u} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : R

The product of sequence values at the half-sum of the first pair and half-difference of the second pair.

Equations

• EllSequence.HaveSameParity₄.addMulSub₄ W a b c d = W ((a + b).tdiv 2) * W ((c - d).tdiv 2)

theorem EllSequence.HaveSameParity₄.addMulSub₄_mul_addMulSub₄ {R : Type u} [CommRing R] {W : ℤ → R} {a b c d : ℤ} : addMulSub₄ W a b c d * addMulSub₄ W c d a b = addMulSub W a b * addMulSub W c d

theorem EllSequence.HaveSameParity₄.addMulSub_transf {R : Type u} [CommRing R] {W : ℤ → R} {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : addMulSub W (avg₄ a b c d - d) (avg₄ a b c d - c) = addMulSub₄ W a b c d ∧ addMulSub W (avg₄ a b c d - d) (avg₄ a b c d - b) = addMulSub₄ W a c b d ∧ addMulSub W (avg₄ a b c d - d) |avg₄ a b c d - a| = addMulSub₄ W b c a d ∧ addMulSub W (avg₄ a b c d - c) (avg₄ a b c d - b) = addMulSub₄ W a d b c ∧ addMulSub W (avg₄ a b c d - c) |avg₄ a b c d - a| = addMulSub₄ W b d a c ∧ addMulSub W (avg₄ a b c d - b) |avg₄ a b c d - a| = addMulSub₄ W c d a b

theorem EllSequence.HaveSameParity₄.rel₄_transf {R : Type u} [CommRing R] {W : ℤ → R} {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : rel₄ W (avg₄ a b c d - d) (avg₄ a b c d - c) (avg₄ a b c d - b) |avg₄ a b c d - a| = rel₄ W a b c d

theorem EllSequence.HaveSameParity₄.transf {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : HaveSameParity₄ (avg₄ a b c d - d) (avg₄ a b c d - c) (avg₄ a b c d - b) |avg₄ a b c d - a|

theorem EllSequence.HaveSameParity₄.strictAnti₄_transf {a b c d : ℤ} (same : HaveSameParity₄ a b c d) (anti : StrictAnti₄ a b c d) : StrictAnti₄ (avg₄ a b c d - d) (avg₄ a b c d - c) (avg₄ a b c d - b) |avg₄ a b c d - a|

def EllSequence.rel₆ {R : Type u} [CommRing R] (W : ℤ → R) (k l a b c d : ℤ) : R

The four-index relation multiplied by a further half-sum and half-difference product.

Equations

• EllSequence.rel₆ W k l a b c d = EllSequence.addMulSub W k l * EllSequence.rel₄ W a b c d

theorem EllSequence.rel₃_iff₄ {R : Type u} [CommRing R] (W : ℤ → R) (m n r : ℤ) : Rel₃ W m n r ↔ rel₄ W (2 * m) (2 * n) (2 * r) 0 = 0

theorem EllSequence.rel₆_eq₃ {R : Type u} [CommRing R] (W : ℤ → R) (c d m n r : ℤ) : rel₆ W c d m n r c = rel₆ W m c n r c d - rel₆ W n c m r c d + rel₆ W r c m n c d

theorem EllSequence.rel₆_eq₃' {R : Type u} [CommRing R] (W : ℤ → R) (c d m n r : ℤ) : rel₆ W c d m n r d = rel₆ W m d n r c d - rel₆ W n d m r c d + rel₆ W r d m n c d

theorem EllSequence.rel₆_eq₁₀ {R : Type u} [CommRing R] (W : ℤ → R) (c d m n r s : ℤ) : rel₆ W c d m n r s = rel₆ W n d m r s c - rel₆ W r d m n s c + rel₆ W s d m n r c + rel₆ W n c m r s d - rel₆ W r c m n s d + rel₆ W s c m n r d + rel₆ W n r m s c d - rel₆ W n s m r c d + rel₆ W r s m n c d - 2 * rel₆ W m d n r s c

theorem EllSequence.addMulSub_sq_mul_rel₄_eq₉ {R : Type u} [CommRing R] (W : ℤ → R) (c d m n r s : ℤ) : addMulSub W c d ^ 2 * rel₄ W m n r s = addMulSub W m c * (rel₆ W n d r s c d - rel₆ W r d n s c d + rel₆ W s d n r c d) - addMulSub W m d * (rel₆ W n c r s c d - rel₆ W r c n s c d + rel₆ W s c n r c d) + addMulSub W c d * (rel₆ W n r m s c d - rel₆ W n s m r c d + rel₆ W r s m n c d)

def EllSequence.OddRec {R : Type u} [CommRing R] (W : ℤ → R) (m : ℤ) : Prop

The odd-index doubling recurrence for an elliptic sequence.

Equations

• EllSequence.OddRec W m = (W (2 * m + 1) * W 1 ^ 3 = W (m + 2) * W m ^ 3 - W (m - 1) * W (m + 1) ^ 3)

def EllSequence.EvenRec {R : Type u} [CommRing R] (W : ℤ → R) (m : ℤ) : Prop

The even-index doubling recurrence for an elliptic sequence.

Equations

• EllSequence.EvenRec W m = (W (2 * m) * W 2 * W 1 ^ 2 = W m * (W (m - 1) ^ 2 * W (m + 2) - W (m - 2) * W (m + 1) ^ 2))

theorem EllSequence.rel₃_iff_oddRec {R : Type u} [CommRing R] (W : ℤ → R) (m : ℤ) : Rel₃ W (m + 1) m 1 ↔ OddRec W m

theorem EllSequence.rel₃_iff_evenRec {R : Type u} [CommRing R] (W : ℤ → R) (m : ℤ) : Rel₃ W (m + 1) (m - 1) 1 ↔ EvenRec W m

theorem EllSequence.rel₄_iff_evenRec {R : Type u} [CommRing R] (W : ℤ → R) (m : ℤ) : rel₄ W (2 * m + 1) (2 * m - 1) 3 1 = 0 ↔ EvenRec W m

def EllSequence.dMin (a : ℤ) : ℤ

The least nonnegative index of the same parity as the given index.

Equations

• EllSequence.dMin a = if Even a then 0 else 1

def EllSequence.cMin (a : ℤ) : ℤ

The next nonnegative index of the same parity after dMin.

Equations

• EllSequence.cMin a = EllSequence.dMin a + 2

theorem EllSequence.dMin_nonneg (a : ℤ) : 0 ≤ dMin a

theorem EllSequence.dMin_lt_cMin (a : ℤ) : dMin a < cMin a

theorem EllSequence.negOnePow_cMin_eq_dMin (a : ℤ) : (cMin a).negOnePow = (dMin a).negOnePow

theorem EllSequence.negOnePow_dMin (a : ℤ) : (dMin a).negOnePow = a.negOnePow

theorem EllSequence.negOnePow_cMin (a : ℤ) : (cMin a).negOnePow = a.negOnePow

theorem EllSequence.addMulSub_mem_nonZeroDivisors {R : Type u} [CommRing R] {W : ℤ → R} (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (a : ℤ) : addMulSub W (cMin a) (dMin a) ∈ nonZeroDivisors R

theorem EllSequence.dMin_le {a b : ℤ} (same : a.negOnePow = b.negOnePow) (h : 0 ≤ b) : dMin a ≤ b

def EllSequence.Rel₄OfValid {R : Type u} [CommRing R] (W : ℤ → R) (a b c d : ℤ) : Prop

The four-index relation vanishes for strictly decreasing nonnegative indices of the same parity.

Equations

• EllSequence.Rel₄OfValid W a b c d = (EllSequence.HaveSameParity₄ a b c d → EllSequence.StrictAnti₄ a b c d → EllSequence.rel₄ W a b c d = 0)

theorem EllSequence.rel₄_fix₁_of_fix₂ {R : Type u} [CommRing R] {W : ℤ → R} {a c₀ d₀ : ℤ} (par : c₀.negOnePow = d₀.negOnePow) (le : 0 ≤ d₀) (lt : d₀ < c₀) (rel : ∀ {a' b : ℤ}, a' ≤ a → Rel₄OfValid W a' b c₀ d₀) (mem : addMulSub W c₀ d₀ ∈ nonZeroDivisors R) (b c : ℤ) : Rel₄OfValid W a b c c₀ ∧ (c₀ < c → Rel₄OfValid W a b c d₀)

theorem EllSequence.rel₄_of_fix₂ {R : Type u} [CommRing R] {W : ℤ → R} {a c₀ d₀ : ℤ} (par : c₀.negOnePow = d₀.negOnePow) (le : 0 ≤ d₀) (lt : d₀ < c₀) (rel : ∀ {a' b : ℤ}, a' ≤ a → Rel₄OfValid W a' b c₀ d₀) (mem : addMulSub W c₀ d₀ ∈ nonZeroDivisors R) (b c d : ℤ) (hc : c₀ < d) (par' : d.negOnePow = d₀.negOnePow) : Rel₄OfValid W a b c d

theorem EllSequence.rel₄_of_min₂ {R : Type u} [CommRing R] {W : ℤ → R} {a : ℤ} (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (rel : ∀ {a' b : ℤ}, a' ≤ a → Rel₄OfValid W a' b (cMin a) (dMin a)) (b c d : ℤ) : Rel₄OfValid W a b c d

theorem EllSequence.rel₄_of_anti_oddRec_evenRec {R : Type u} [CommRing R] {W : ℤ → R} (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (oddRec : ∀ m ≥ 2, OddRec W m) (evenRec : ∀ m ≥ 3, EvenRec W m) ⦃a b c d : ℤ⦄ : Rel₄OfValid W a b c d

theorem EllSequence.rel₄_abs {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) {m n r s : ℤ} : rel₄ W |m| |n| |r| |s| = rel₄ W m n r s

theorem EllSequence.rel₄_swap₀₁ {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) {m n r s : ℤ} : rel₄ W m n r s = -rel₄ W n m r s

theorem EllSequence.rel₄_swap₁₂ {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) {m n r s : ℤ} : rel₄ W m n r s = -rel₄ W m r n s

theorem EllSequence.rel₄_swap₂₃ {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) {m n r s : ℤ} : rel₄ W m n r s = -rel₄ W m n s r

def EllSequence.relFin4 {R : Type u} [CommRing R] (W : ℤ → R) (t : Fin 4 → ℤ) : R

The four-index relation with its arguments packaged as a function on Fin 4.

Equations

• EllSequence.relFin4 W t = EllSequence.rel₄ W (t 0) (t 1) (t 2) (t 3)

theorem EllSequence.relFin4_perm {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) (σ : Equiv.Perm (Fin 4)) (t : Fin 4 → ℤ) : relFin4 W (t ∘ ⇑σ) = Equiv.Perm.sign σ • relFin4 W t

theorem EllSequence.relFin4_perm' {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) (σ : Equiv.Perm (Fin 4)) (t : Fin 4 → ℤ) : Equiv.Perm.sign σ • relFin4 W (t ∘ ⇑σ) = relFin4 W t

theorem EllSequence.rel₄_same₀₁ {R : Type u} [CommRing R] {W : ℤ → R} (zero : W 0 = 0) (m r s : ℤ) : rel₄ W m m r s = 0

theorem EllSequence.rel₄_same₁₂ {R : Type u} [CommRing R] {W : ℤ → R} (zero : W 0 = 0) (m n s : ℤ) : rel₄ W m n n s = 0

theorem EllSequence.rel₄_same₂₃ {R : Type u} [CommRing R] {W : ℤ → R} (zero : W 0 = 0) (m n r : ℤ) : rel₄ W m n r r = 0

theorem EllSequence.rel₄_of_oddRec_evenRec {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) (zero : W 0 = 0) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (oddRec : ∀ m ≥ 2, OddRec W m) (evenRec : ∀ m ≥ 3, EvenRec W m) {a b c d : ℤ} (same : HaveSameParity₄ a b c d) : rel₄ W a b c d = 0

theorem IsEllipticSequence.of_oddRec_evenRec {R : Type u} [CommRing R] {W : ℤ → R} (neg : ∀ (k : ℤ), W (-k) = -W k) (zero : W 0 = 0) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (oddRec : ∀ m ≥ 2, EllSequence.OddRec W m) (evenRec : ∀ m ≥ 3, EllSequence.EvenRec W m) : IsEllipticSequence W

theorem IsEllipticSequence.oddRec {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (m : ℤ) : EllSequence.OddRec W m

theorem IsEllipticSequence.evenRec {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (m : ℤ) : EllSequence.EvenRec W m

theorem IsEllipticSequence.zero' {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) [IsReduced R] : W 0 = 0

theorem IsEllipticSequence.zero {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (m : ℤ) (mem : W (2 * m) ∈ nonZeroDivisors R) : W 0 = 0

theorem IsEllipticSequence.sub_add_neg_sub_mul_eq_zero {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (m n r : ℤ) : (W (m - n) + W (-(m - n))) * W (m + n) * W r ^ 2 = 0

theorem IsEllipticSequence.neg {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (m : ℤ) : W (-m) = -W m

theorem IsEllipticSequence.rel₄ {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) {a b c d : ℤ} (same : EllSequence.HaveSameParity₄ a b c d) : EllSequence.rel₄ W a b c d = 0

theorem IsEllipticSequence.net {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (p q r s : ℤ) : EllSequence.net W p q r s = 0

theorem IsEllipticSequence.invar {R : Type u} [CommRing R] {W : ℤ → R} (ell : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (s m n : ℤ) : EllSequence.invarNum W s m * EllSequence.invarDenom W s n = EllSequence.invarNum W s n * EllSequence.invarDenom W s m

theorem invarNum_normEDS {R : Type u} [CommRing R] (b c d : R) (n : ℤ) : EllSequence.invarNum (normEDS b c d) 1 n = normEDS b c d (n + 2) * normEDS b c d (n - 1) ^ 2 + normEDS b c d (n + 1) ^ 2 * normEDS b c d (n - 2) + normEDS b c d n ^ 3 * b ^ 2

theorem invarNum_normEDS_two {R : Type u} [CommRing R] (b c d : R) : EllSequence.invarNum (normEDS b c d) 1 2 = (d + b ^ 4) * b

theorem invarDenom_normEDS_two {R : Type u} [CommRing R] (b c d : R) : EllSequence.invarDenom (normEDS b c d) 1 2 = c * b

def compl₂EDSAux {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : R

An auxiliary division-polynomial expression used to define the complementary doubling sequence without division.

Equations

• compl₂EDSAux b c d m = preNormEDS (b ^ 4) c d (m - 2) * preNormEDS (b ^ 4) c d (m + 1) ^ 2 * if Even m then 1 else b

@[simp]

theorem compl₂EDSAux_zero {R : Type u} [CommRing R] (b c d : R) : compl₂EDSAux b c d 0 = -1

@[simp]

theorem compl₂EDSAux_one {R : Type u} [CommRing R] (b c d : R) : compl₂EDSAux b c d 1 = -b

@[simp]

theorem compl₂EDSAux_neg_one {R : Type u} [CommRing R] (b c d : R) : compl₂EDSAux b c d (-1) = 0

@[simp]

theorem compl₂EDSAux_two {R : Type u} [CommRing R] (b c d : R) : compl₂EDSAux b c d 2 = 0

@[simp]

theorem compl₂EDSAux_neg_two {R : Type u} [CommRing R] (b c d : R) : compl₂EDSAux b c d (-2) = -d

theorem compl₂EDSAux_mul_b {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : compl₂EDSAux b c d m * b = normEDS b c d (m - 2) * normEDS b c d (m + 1) ^ 2

def compl₂EDS {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : R

The complementary doubling sequence whose product with the normalized elliptic sequence gives its doubled-index values.

Equations

• compl₂EDS b c d m = (preNormEDS (b ^ 4) c d (m - 1) ^ 2 * preNormEDS (b ^ 4) c d (m + 2) - preNormEDS (b ^ 4) c d (m - 2) * preNormEDS (b ^ 4) c d (m + 1) ^ 2) * if Even m then 1 else b

theorem compl₂EDSAux_neg {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : compl₂EDSAux b c d (-m) = -compl₂EDS b c d m - compl₂EDSAux b c d m

@[simp]

theorem compl₂EDS_zero {R : Type u} [CommRing R] (b c d : R) : compl₂EDS b c d 0 = 2

@[simp]

theorem compl₂EDS_one {R : Type u} [CommRing R] (b c d : R) : compl₂EDS b c d 1 = b

@[simp]

theorem compl₂EDS_two {R : Type u} [CommRing R] (b c d : R) : compl₂EDS b c d 2 = d

@[simp]

theorem compl₂EDS_neg {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : compl₂EDS b c d (-m) = compl₂EDS b c d m

theorem normEDS_mul_compl₂EDS {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : normEDS b c d m * compl₂EDS b c d m = normEDS b c d (2 * m)

theorem normEDS_dvd_two_mul {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : normEDS b c d m ∣ normEDS b c d (2 * m)

theorem compl₂EDS_mul_b {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : compl₂EDS b c d m * b = normEDS b c d (m - 1) ^ 2 * normEDS b c d (m + 2) - normEDS b c d (m - 2) * normEDS b c d (m + 1) ^ 2

theorem normEDS_six_eq_mul {R : Type u} [CommRing R] (b c d : R) : normEDS b c d 6 = (normEDS b c d 5 - d ^ 2) * b * c

@[irreducible]

def EllSequence.compl' {R : Type u} [CommRing R] (W₁ compl₂ : ℤ → R) (m : ℤ) : ℕ → R

The recursively defined complementary sequence on natural indices for a fixed base index.

Equations

• One or more equations did not get rendered due to their size.
• EllSequence.compl' W₁ compl₂ m 0 = 0
• EllSequence.compl' W₁ compl₂ m 1 = 1

def EllSequence.compl {R : Type u} [CommRing R] (W₁ compl₂ : ℤ → R) (m n : ℤ) : R

The odd extension to integer indices of the complementary sequence.

Equations

• EllSequence.compl W₁ compl₂ m n = ↑n.sign * EllSequence.compl' W₁ compl₂ m n.natAbs

theorem EllSequence.compl_ofNat {R : Type u} [CommRing R] (W₁ compl₂ : ℤ → R) (m : ℤ) (n : ℕ) : compl W₁ compl₂ m ↑n = compl' W₁ compl₂ m n

theorem EllSequence.compl_neg {R : Type u} [CommRing R] (W₁ compl₂ : ℤ → R) (m n : ℤ) : compl W₁ compl₂ m (-n) = -compl W₁ compl₂ m n

def EllSequence.complEDS {R : Type u} [CommRing R] (b c d : R) (m n : ℤ) : R

The complementary sequence for normalized elliptic divisibility sequences, multiplying the base-index value to the product-index value.

Equations

• EllSequence.complEDS b c d m = EllSequence.compl (normEDS b c d) (compl₂EDS b c d) m

theorem map_compl₂EDS {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) {b c d : R} (n : ℤ) : f (compl₂EDS b c d n) = compl₂EDS (f b) (f c) (f d) n

theorem EllSequence.map_compl' {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (W₁ compl₂ : ℤ → R) (m : ℤ) (n : ℕ) : f (compl' W₁ compl₂ m n) = compl' (⇑f ∘ W₁) (⇑f ∘ compl₂) m n

theorem EllSequence.map_compl {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (W₁ compl₂ : ℤ → R) (m n : ℤ) : f (compl W₁ compl₂ m n) = compl (⇑f ∘ W₁) (⇑f ∘ compl₂) m n

theorem EllSequence.map_complEDS {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) {b c d : R} (m n : ℤ) : f (complEDS b c d m n) = complEDS (f b) (f c) (f d) m n

theorem map_addMulSub {R : Type u} {S : Type v} [CommRing R] [CommRing S] {W : ℤ → R} {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (m n : ℤ) : f (EllSequence.addMulSub W m n) = EllSequence.addMulSub (⇑f ∘ W) m n

theorem map_rel₄ {R : Type u} {S : Type v} [CommRing R] [CommRing S] {W : ℤ → R} {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (p q r s : ℤ) : f (EllSequence.rel₄ W p q r s) = EllSequence.rel₄ (⇑f ∘ W) p q r s

theorem map_net {R : Type u} {S : Type v} [CommRing R] [CommRing S] {W : ℤ → R} {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (p q r s : ℤ) : f (EllSequence.net W p q r s) = EllSequence.net (⇑f ∘ W) p q r s

theorem map_invarNum {R : Type u} {S : Type v} [CommRing R] [CommRing S] {W : ℤ → R} {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (s m : ℤ) : f (EllSequence.invarNum W s m) = EllSequence.invarNum (⇑f ∘ W) s m

theorem map_invarDenom {R : Type u} {S : Type v} [CommRing R] [CommRing S] {W : ℤ → R} {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (s m : ℤ) : f (EllSequence.invarDenom W s m) = EllSequence.invarDenom (⇑f ∘ W) s m

inductive Param : Type

The three indeterminates parametrizing the universal normalized elliptic divisibility sequence.

• B : Param
• C : Param
• D : Param

noncomputable def universalNormEDS : ℤ → MvPolynomial Param ℤ

The normalized elliptic divisibility sequence over the integer polynomial ring in the three parameters.

Equations

• universalNormEDS = normEDS (MvPolynomial.X Param.B) (MvPolynomial.X Param.C) (MvPolynomial.X Param.D)

theorem normEDS_eq_aeval {R : Type u} [CommRing R] {b c d : R} : normEDS b c d = fun (x : ℤ) => (MvPolynomial.aeval fun (t : Param) => Param.rec b c d t) (universalNormEDS x)

theorem compl₂EDS_eq_aeval {R : Type u} [CommRing R] {b c d : R} : compl₂EDS b c d = fun (x : ℤ) => (MvPolynomial.aeval fun (t : Param) => Param.rec b c d t) (compl₂EDS (MvPolynomial.X Param.B) (MvPolynomial.X Param.C) (MvPolynomial.X Param.D) x)

theorem complEDS_eq_aeval {R : Type u} [CommRing R] {b c d : R} : EllSequence.complEDS b c d = fun (x1 x2 : ℤ) => (MvPolynomial.aeval fun (t : Param) => Param.rec b c d t) (EllSequence.complEDS (MvPolynomial.X Param.B) (MvPolynomial.X Param.C) (MvPolynomial.X Param.D) x1 x2)

theorem IsEllipticSequence.normEDS {R : Type u} [CommRing R] {b c d : R} : IsEllipticSequence (normEDS b c d)

theorem IsEllipticSequence.ext {R : Type u} [CommRing R] {W U : ℤ → R} (ellW : IsEllipticSequence W) (ellU : IsEllipticSequence U) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (h1 : W 1 = U 1) (h2 : W 2 = U 2) (h3 : W 3 = U 3) (h4 : W 4 = U 4) : W = U

theorem normEDS_two_three_two : normEDS 2 3 2 = id

theorem compl₂EDS_two_three_two (n : ℤ) : compl₂EDS 2 3 2 n = 2

theorem universalNormEDS_ne_zero {n : ℤ} (hn : n ≠ 0) : universalNormEDS n ≠ 0

theorem universalNormEDS_mem_nonZeroDivisors {n : ℤ} (hn : n ≠ 0) : universalNormEDS n ∈ nonZeroDivisors (MvPolynomial Param ℤ)

theorem IsEllipticSequence.eq_normEDS_of_dvd {R : Type u} [CommRing R] {W : ℤ → R} (ellW : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (dvd₁₂ : W 1 ∣ W 2) (dvd₁₃ : W 1 ∣ W 3) (dvd₂₄ : W 2 ∣ W 4) : ∃ (b : R) (c : R) (d : R), W = fun (x : ℤ) => W 1 * normEDS b c d x

theorem IsEllipticDvdSequence.eq_normEDS {R : Type u} [CommRing R] {W : ℤ → R} (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (h : IsEllipticDvdSequence W) : ∃ (b : R) (c : R) (d : R), W = fun (x : ℤ) => W 1 * normEDS b c d x

theorem IsEllipticSequence.mul_compl_eq_apply_mul_of_mem_nonZeroDivisors {R : Type u} [CommRing R] {W : ℤ → R} (ellW : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (W₁ compl₂ : ℤ → R) (h₁ : ∀ (m : ℤ), W 1 * W₁ m = W m) (h₂ : ∀ (m : ℤ), W m * compl₂ m = W (2 * m)) (m n : ℤ) (mem : W m ∈ nonZeroDivisors R) : W m * EllSequence.compl W₁ compl₂ m n = W (n * m)

theorem normEDS_mul_complEDS {R : Type u} [CommRing R] {b c d : R} (m n : ℤ) : normEDS b c d m * EllSequence.complEDS b c d m n = normEDS b c d (n * m)

theorem normEDS_mul_complEDS_div {R : Type u} [CommRing R] {b c d : R} (m : ℤ) (hm : m ≠ 0) (n : ℤ) (dvd : m ∣ n) : normEDS b c d m * EllSequence.complEDS b c d m (n / m) = normEDS b c d n

def EllSequence.redInvarNum {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : R

The reduced numerator obtained by removing the universal factor from the invariant numerator at first index one.

Equations

• EllSequence.redInvarNum b c d m = compl₂EDS b c d m + normEDS b c d m ^ 3 * b + 2 * compl₂EDSAux b c d m

theorem EllSequence.compl₂EDS_eq_redInvarNum_sub {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : compl₂EDS b c d m = redInvarNum b c d m - normEDS b c d m ^ 3 * b - 2 * compl₂EDSAux b c d m

theorem EllSequence.invarNum_eq_redInvarNum_mul {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : invarNum (normEDS b c d) 1 m = redInvarNum b c d m * b

def EllSequence.redInvarDenom {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : R

The reduced denominator obtained by removing the universal factors from the invariant denominator at first index one.

Equations

• One or more equations did not get rendered due to their size.

theorem EllSequence.invarDenom_eq_redInvarDenom_mul {R : Type u} [CommRing R] (b c d : R) (m : ℤ) : invarDenom (normEDS b c d) 1 m = redInvarDenom b c d m * b * c

@[simp]

theorem EllSequence.redInvarDenom_zero {R : Type u} [CommRing R] (b c d : R) : redInvarDenom b c d 0 = 0

@[simp]

theorem EllSequence.redInvarDenom_one {R : Type u} [CommRing R] (b c d : R) : redInvarDenom b c d 1 = 0

@[simp]

theorem EllSequence.redInvarDenom_two {R : Type u} [CommRing R] (b c d : R) : redInvarDenom b c d 2 = 1

theorem EllSequence.map_compl₂EDSAux {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (m : ℤ) : f (compl₂EDSAux b c d m) = compl₂EDSAux (f b) (f c) (f d) m

theorem EllSequence.map_redInvarNum {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (m : ℤ) : f (redInvarNum b c d m) = redInvarNum (f b) (f c) (f d) m

theorem EllSequence.map_redInvarDenom {R : Type u} {S : Type v} [CommRing R] [CommRing S] {F : Type u_1} [FunLike F R S] [RingHomClass F R S] (f : F) (b c d : R) (m : ℤ) : f (redInvarDenom b c d m) = redInvarDenom (f b) (f c) (f d) m

theorem IsDvdSequence.normEDS {R : Type u} [CommRing R] {b c d : R} : IsDvdSequence (normEDS b c d)

theorem IsEllipticDvdSequence.normEDS {R : Type u} [CommRing R] {b c d : R} : IsEllipticDvdSequence (normEDS b c d)

theorem IsEllipticSequence.isDivSequence_of_dvd {R : Type u} [CommRing R] {W : ℤ → R} (ellW : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (dvd₁₂ : W 1 ∣ W 2) (dvd₁₃ : W 1 ∣ W 3) (dvd₂₄ : W 2 ∣ W 4) : IsDvdSequence W

theorem IsEllipticSequence.isEllDivSequence_of_dvd {R : Type u} [CommRing R] {W : ℤ → R} (ellW : IsEllipticSequence W) (one : W 1 ∈ nonZeroDivisors R) (two : W 2 ∈ nonZeroDivisors R) (dvd₁₂ : W 1 ∣ W 2) (dvd₁₃ : W 1 ∣ W 3) (dvd₂₄ : W 2 ∣ W 4) : IsEllipticDvdSequence W

theorem net_normEDS {R : Type u} [CommRing R] {b c d : R} (p q r s : ℤ) : EllSequence.net (normEDS b c d) p q r s = 0

theorem rel₄_normEDS {R : Type u} [CommRing R] {b c d : R} (p q r s : ℤ) (same : EllSequence.HaveSameParity₄ p q r s) : EllSequence.rel₄ (normEDS b c d) p q r s = 0

theorem invar_normEDS {R : Type u} [CommRing R] {b c d : R} (s m n : ℤ) : EllSequence.invarNum (normEDS b c d) s m * EllSequence.invarDenom (normEDS b c d) s n = EllSequence.invarNum (normEDS b c d) s n * EllSequence.invarDenom (normEDS b c d) s m

theorem invar₂_normEDS {R : Type u} [CommRing R] {b c d : R} {m : ℤ} : EllSequence.invarNum (normEDS b c d) 1 m * c = EllSequence.invarDenom (normEDS b c d) 1 m * (d + b ^ 4)

theorem redInvar_normEDS {R : Type u} [CommRing R] {b c d : R} (m : ℤ) : EllSequence.redInvarNum b c d m = EllSequence.redInvarDenom b c d m * (d + b ^ 4)

inductive WeierstrassCurve.Coeff : Type

The five coefficient labels for a Weierstrass equation.

• A₁ : Coeff
• A₂ : Coeff
• A₃ : Coeff
• A₄ : Coeff
• A₆ : Coeff

theorem WeierstrassCurve.Affine.CoordinateRing.algebraMap_injective' {R : Type u_1} [CommRing R] (W : Affine R) : Function.Injective ⇑(algebraMap R W.CoordinateRing)

noncomputable def WeierstrassCurve.Univ.curve : Affine (MvPolynomial Coeff ℤ)

The universal Weierstrass curve over the integer polynomial ring in its five coefficients.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Univ.Δ_curve_ne_zero : Δ curve ≠ 0

@[reducible, inline]

abbrev WeierstrassCurve.Univ.Poly : Type

The bivariate polynomial ring for affine coordinates of the universal curve.

Equations

• WeierstrassCurve.Univ.Poly = Polynomial (Polynomial (MvPolynomial WeierstrassCurve.Coeff ℤ))

@[reducible, inline]

abbrev WeierstrassCurve.Univ.Ring : Type

The coordinate ring of the universal Weierstrass curve.

Equations

• WeierstrassCurve.Univ.Ring = WeierstrassCurve.Univ.curve.CoordinateRing

@[reducible, inline]

abbrev WeierstrassCurve.Univ.Field : Type

The fraction field of the universal curve's coordinate ring.

Equations

• WeierstrassCurve.Univ.Field = FractionRing WeierstrassCurve.Univ.Ring

@[instance_reducible]

noncomputable instance WeierstrassCurve.Univ.instCommRingPoly : CommRing Poly

Equations

• WeierstrassCurve.Univ.instCommRingPoly = Polynomial.commRing

theorem WeierstrassCurve.Univ.Poly.two_ne_zero : 2 ≠ 0

noncomputable def WeierstrassCurve.Univ.polyToField : Poly →+* Univ.Field

The map from coordinate polynomials to the function field of the universal curve.

Equations

• WeierstrassCurve.Univ.polyToField = (algebraMap WeierstrassCurve.Univ.Ring WeierstrassCurve.Univ.Field).comp (AdjoinRoot.mk WeierstrassCurve.Univ.curve.polynomial)

theorem WeierstrassCurve.Univ.polyToField_apply (p : Poly) : polyToField p = (algebraMap Univ.Ring Univ.Field) ((AdjoinRoot.mk curve.polynomial) p)

theorem WeierstrassCurve.Univ.algebraMap_field_eq_comp : algebraMap (MvPolynomial Coeff ℤ) Univ.Field = polyToField.comp (algebraMap (MvPolynomial Coeff ℤ) Poly)

theorem WeierstrassCurve.Univ.algebraMap_ring_eq_comp : algebraMap (MvPolynomial Coeff ℤ) Univ.Ring = (AdjoinRoot.mk curve.polynomial).comp (algebraMap (MvPolynomial Coeff ℤ) (Polynomial (Polynomial (MvPolynomial Coeff ℤ))))

@[simp]

theorem WeierstrassCurve.Univ.polyToField_polynomial : polyToField curve.polynomial = 0

theorem WeierstrassCurve.Univ.algebraMap_field_injective : Function.Injective ⇑(algebraMap (MvPolynomial Coeff ℤ) Univ.Field)

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.pointedCurve : WeierstrassCurve Univ.Field

The universal curve base-changed to its own function field.

Equations

• WeierstrassCurve.Univ.pointedCurve = WeierstrassCurve.baseChange WeierstrassCurve.Univ.curve WeierstrassCurve.Univ.Field

instance WeierstrassCurve.Univ.instIsEllipticFieldPointedCurve : pointedCurve.IsElliptic

theorem WeierstrassCurve.Univ.equation_point : pointedCurve.toAffine.Equation (polyToField (Polynomial.C Polynomial.X)) (polyToField Polynomial.X)

noncomputable def WeierstrassCurve.Univ.Affine.point : (curve.baseChange Univ.Field).Point

The generic affine point of the universal curve over its function field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def WeierstrassCurve.Univ.Jacobian.point : Jacobian.Point (baseChange curve Univ.Field)

The generic point of the universal curve in Jacobian coordinates.

Equations

• WeierstrassCurve.Univ.Jacobian.point = WeierstrassCurve.Jacobian.Point.fromAffine WeierstrassCurve.Univ.Affine.point

@[simp]

theorem WeierstrassCurve.Univ.pointedCurve_a₁ : pointedCurve.a₁ = polyToField (Polynomial.CC curve.a₁)

@[simp]

theorem WeierstrassCurve.Univ.pointedCurve_a₂ : pointedCurve.a₂ = polyToField (Polynomial.CC curve.a₂)

@[simp]

theorem WeierstrassCurve.Univ.pointedCurve_a₃ : pointedCurve.a₃ = polyToField (Polynomial.CC curve.a₃)

@[simp]

theorem WeierstrassCurve.Univ.pointedCurve_a₄ : pointedCurve.a₄ = polyToField (Polynomial.CC curve.a₄)

@[simp]

theorem WeierstrassCurve.Univ.pointedCurve_a₆ : pointedCurve.a₆ = polyToField (Polynomial.CC curve.a₆)

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.curvePoly : WeierstrassCurve Poly

The universal curve base-changed to the coordinate polynomial ring.

Equations

• WeierstrassCurve.Univ.curvePoly = WeierstrassCurve.baseChange WeierstrassCurve.Univ.curve WeierstrassCurve.Univ.Poly

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.curveRing : WeierstrassCurve Univ.Ring

The universal curve base-changed to its coordinate ring.

Equations

• WeierstrassCurve.Univ.curveRing = WeierstrassCurve.baseChange WeierstrassCurve.Univ.curve WeierstrassCurve.Univ.Ring

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.curveField : WeierstrassCurve Univ.Field

The universal curve base-changed to its function field.

Equations

• WeierstrassCurve.Univ.curveField = WeierstrassCurve.baseChange WeierstrassCurve.Univ.curve WeierstrassCurve.Univ.Field

theorem WeierstrassCurve.Univ.curveField_eq : curveField = pointedCurve

def WeierstrassCurve.cusp : Affine ℤ

The cuspidal Weierstrass equation y² = x³ over the integers.

Equations

• WeierstrassCurve.cusp = { a₁ := 0, a₂ := 0, a₃ := 0, a₄ := 0, a₆ := 0 }

theorem WeierstrassCurve.cusp_equation_one_one : cusp.Equation 1 1

noncomputable def WeierstrassCurve.specialize {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : MvPolynomial Coeff ℤ →+* R

Evaluate the five universal coefficient variables at the coefficients of the given curve.

Equations

• W.specialize = (MvPolynomial.aeval fun (t : WeierstrassCurve.Coeff) => WeierstrassCurve.Coeff.rec W.a₁ W.a₂ W.a₃ W.a₄ W.a₆ t).toRingHom

theorem WeierstrassCurve.map_specialize {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : map Univ.curve W.specialize = W

noncomputable def WeierstrassCurve.Univ.polyEval {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) : Poly →+* R

Evaluate the universal coefficient and coordinate variables at the given curve and coordinates.

Equations

• WeierstrassCurve.Univ.polyEval W x y = Polynomial.eval₂RingHom (Polynomial.eval₂RingHom W.specialize x) y

theorem WeierstrassCurve.Univ.polyEval_apply {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) (p : Poly) : (polyEval W x y) p = Polynomial.evalEval x y (Polynomial.map (Polynomial.mapRingHom W.specialize) p)

noncomputable def WeierstrassCurve.Univ.ringEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : Univ.Ring →+* R

Evaluate the universal coordinate ring at a point satisfying the given curve equation.

Equations

• WeierstrassCurve.Univ.ringEval eqn = AdjoinRoot.lift (Polynomial.eval₂RingHom W.specialize x) y ⋯

theorem WeierstrassCurve.Univ.ringEval_mk {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) (p : Poly) : (ringEval eqn) ((AdjoinRoot.mk curve.polynomial) p) = (polyEval W x y) p

theorem WeierstrassCurve.Univ.ringEval_comp_mk {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : (ringEval eqn).comp (AdjoinRoot.mk curve.polynomial) = polyEval W x y

theorem WeierstrassCurve.Univ.polyEval_comp_eq_specialize {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} : (polyEval W x y).comp (algebraMap (MvPolynomial Coeff ℤ) Poly) = W.specialize

theorem WeierstrassCurve.Univ.ringEval_comp_eq_specialize {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : (ringEval eqn).comp (algebraMap (MvPolynomial Coeff ℤ) Univ.Ring) = W.specialize

theorem WeierstrassCurve.Univ.Field.two_ne_zero : 2 ≠ 0

theorem WeierstrassCurve.Univ.curveRing_map_ringEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : Affine.Equation W x y) : curveRing.map (ringEval eqn) = W

noncomputable def WeierstrassCurve.invar {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Polynomial R

The polynomial 6X² + b₂X + b₄ used in the division-sequence invariant.

Equations

• W.invar = 6 * Polynomial.X ^ 2 + Polynomial.C W.b₂ * Polynomial.X + Polynomial.C W.b₄

noncomputable def WeierstrassCurve.ψc {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : ℤ → Polynomial (Polynomial R)

The complementary division polynomial whose product with ψₙ is ψ₂ₙ.

Equations

• W.ψc = compl₂EDS W.ψ₂ (Polynomial.C W.Ψ₃) (Polynomial.C W.preΨ₄)

theorem WeierstrassCurve.C_Ψ₃_eq {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Polynomial.C W.Ψ₃ = (3 * Polynomial.C Polynomial.X + Polynomial.CC W.a₂) * Polynomial.C W.Ψ₂Sq - Affine.polynomialX W ^ 2 + Polynomial.CC W.a₁ * W.ψ₂ * Affine.polynomialX W - Polynomial.CC W.a₁ ^ 2 * Affine.polynomial W

theorem WeierstrassCurve.preΨ₄_add_Ψ₂Sq_sq {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.preΨ₄ + W.Ψ₂Sq ^ 2 = W.invar * W.Ψ₃

theorem WeierstrassCurve.preΨ₄_add_ψ₂_pow_four {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Polynomial.C W.preΨ₄ + W.ψ₂ ^ 4 = Polynomial.C (W.invar * W.Ψ₃) + 8 * Affine.polynomial W * (2 * Affine.polynomial W + Polynomial.C W.Ψ₂Sq)

theorem WeierstrassCurve.φ_mul_ψ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.φ n * W.ψ n = Polynomial.C Polynomial.X * W.ψ n ^ 3 - EllSequence.invarDenom W.ψ 1 n

noncomputable def WeierstrassCurve.ωe {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : Polynomial (Polynomial R)

The polynomial numerator for the y-coordinate of multiplication by an integer.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.ωe_spec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : 2 * W.ωe n + Polynomial.CC W.a₁ * W.φ n * W.ψ n + Polynomial.CC W.a₃ * W.ψ n ^ 3 = W.ψc n

theorem WeierstrassCurve.two_mul_ωe {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : 2 * W.ωe n = W.ψc n - Polynomial.CC W.a₁ * W.φ n * W.ψ n - Polynomial.CC W.a₃ * W.ψ n ^ 3

theorem WeierstrassCurve.ψc_spec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.ψ n * W.ψc n = W.ψ (2 * n)

@[simp]

theorem WeierstrassCurve.ωe_zero {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.ωe 0 = 1

@[simp]

theorem WeierstrassCurve.ωe_one {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.ωe 1 = Polynomial.X

@[simp]

theorem WeierstrassCurve.ψc_neg {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (n : ℤ) : W.ψc (-n) = W.ψc n

theorem WeierstrassCurve.map_ψc {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).ψc n = Polynomial.map (Polynomial.mapRingHom f) (W.ψc n)

theorem WeierstrassCurve.map_invar {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) : (W.map f).invar = Polynomial.map f W.invar

theorem WeierstrassCurve.map_ωe {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ) : (W.map f).ωe n = Polynomial.map (Polynomial.mapRingHom f) (W.ωe n)

theorem WeierstrassCurve.Univ.evalEval_ψ₂ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : Polynomial.evalEval x y W.ψ₂ = (polyEval W x y) (ψ₂ curve)

theorem WeierstrassCurve.Univ.evalEval_Ψ₃ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : Polynomial.evalEval x y (Polynomial.C W.Ψ₃) = (polyEval W x y) (Polynomial.C (Ψ₃ curve))

theorem WeierstrassCurve.Univ.evalEval_preΨ₄ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} : Polynomial.evalEval x y (Polynomial.C W.preΨ₄) = (polyEval W x y) (Polynomial.C (preΨ₄ curve))

theorem WeierstrassCurve.Univ.evalEval_ψ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.ψ n) = (polyEval W x y) (WeierstrassCurve.ψ curve n)

theorem WeierstrassCurve.Univ.evalEval_φ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.φ n) = (polyEval W x y) (WeierstrassCurve.φ curve n)

theorem WeierstrassCurve.Univ.evalEval_ωe {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) {x y : R} {n : ℤ} : Polynomial.evalEval x y (W.ωe n) = (polyEval W x y) (WeierstrassCurve.ωe curve n)

theorem WeierstrassCurve.Univ.cusp_ψ₂ : ψ₂ cusp = 2 * Polynomial.X

theorem WeierstrassCurve.Univ.cusp_Ψ₃ : Ψ₃ cusp = 3 * Polynomial.X ^ 4

theorem WeierstrassCurve.Univ.cusp_preΨ₄ : preΨ₄ cusp = 2 * Polynomial.X ^ 6

theorem WeierstrassCurve.Univ.polyEval_cusp_ψ {n : ℤ} : (polyEval cusp 1 1) (WeierstrassCurve.ψ curve n) = n

theorem WeierstrassCurve.Univ.polyEval_cusp_φ {n : ℤ} : (polyEval cusp 1 1) (WeierstrassCurve.φ curve n) = 1

theorem WeierstrassCurve.Univ.polyEval_cusp_ψc {n : ℤ} : (polyEval cusp 1 1) (ψc curve n) = 2

theorem WeierstrassCurve.Univ.polyEval_cusp_ωe {n : ℤ} : (polyEval cusp 1 1) (WeierstrassCurve.ωe curve n) = 1

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.ψᵤ (n : ℤ) : Univ.Field

The division sequence of the universal curve viewed in its function field.

Equations

• WeierstrassCurve.Univ.ψᵤ n = WeierstrassCurve.Univ.polyToField (WeierstrassCurve.ψ WeierstrassCurve.Univ.curve n)

theorem WeierstrassCurve.Univ.ψᵤ_eq_normEDS : ψᵤ = normEDS (polyToField (ψ₂ curve)) (polyToField (Polynomial.C (Ψ₃ curve))) (polyToField (Polynomial.C (preΨ₄ curve)))

theorem WeierstrassCurve.Univ.isEllSequence_ψᵤ : IsEllipticSequence ψᵤ

theorem WeierstrassCurve.Univ.net_ψᵤ (p q r s : ℤ) : EllSequence.net ψᵤ p q r s = 0

theorem WeierstrassCurve.Univ.ψᵤ_ne_zero {n : ℤ} (h0 : n ≠ 0) : ψᵤ n ≠ 0

theorem WeierstrassCurve.Univ.polyToField_φ_ne_zero {n : ℤ} : polyToField (WeierstrassCurve.φ curve n) ≠ 0

theorem WeierstrassCurve.Univ.polyToField_ψ₂Sq : polyToField (Polynomial.C (Ψ₂Sq curve)) = ψᵤ 2 ^ 2

noncomputable def WeierstrassCurve.Univ.Affine.smulX (n : ℤ) : Univ.Field

The candidate multiplication-map x-coordinate φₙ / ψₙ² at the generic point.

Equations

• WeierstrassCurve.Univ.Affine.smulX n = WeierstrassCurve.Univ.polyToField (WeierstrassCurve.φ WeierstrassCurve.Univ.curve n) / WeierstrassCurve.Univ.ψᵤ n ^ 2

noncomputable def WeierstrassCurve.Univ.Affine.smulY (n : ℤ) : Univ.Field

The candidate multiplication-map y-coordinate ωₙ / ψₙ³ at the generic point.

Equations

• WeierstrassCurve.Univ.Affine.smulY n = WeierstrassCurve.Univ.polyToField (WeierstrassCurve.ωe WeierstrassCurve.Univ.curve n) / WeierstrassCurve.Univ.ψᵤ n ^ 3

@[simp]

theorem WeierstrassCurve.Univ.Affine.smulX_zero : smulX 0 = 0

@[simp]

theorem WeierstrassCurve.Univ.Affine.smulY_zero : smulY 0 = 0

@[simp]

theorem WeierstrassCurve.Univ.Affine.smulX_one : smulX 1 = polyToField (Polynomial.C Polynomial.X)

@[simp]

theorem WeierstrassCurve.Univ.Affine.smulY_one : smulY 1 = polyToField Polynomial.X

theorem WeierstrassCurve.Univ.Affine.smulX_eq {n : ℤ} (hn : n ≠ 0) : smulX n = smulX 1 - ψᵤ (n + 1) * ψᵤ (n - 1) / ψᵤ n ^ 2

theorem WeierstrassCurve.Univ.Affine.smulX_two : smulX 2 = smulX 1 - ψᵤ 3 / ψᵤ 2 ^ 2

theorem WeierstrassCurve.Univ.Affine.smulX_sub_smulX {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) : smulX m - smulX n = ψᵤ (n + m) * ψᵤ (n - m) / (ψᵤ n * ψᵤ m) ^ 2

theorem WeierstrassCurve.Univ.Affine.smulX_sub_sub_smulX_add {m n : ℤ} (add_ne : n + m ≠ 0) (sub_ne : n - m ≠ 0) : smulX (n - m) - smulX (n + m) = ψᵤ (2 * n) * ψᵤ (2 * m) / (ψᵤ (n + m) * ψᵤ (n - m)) ^ 2

theorem WeierstrassCurve.Univ.Affine.smulX_neg {n : ℤ} : smulX (-n) = smulX n

theorem WeierstrassCurve.Univ.Affine.smulX_ne_zero {n : ℤ} (h0 : n ≠ 0) : smulX n ≠ 0

theorem WeierstrassCurve.Univ.Affine.smulX_ne_smulX {m n : ℤ} (ne : m ≠ n) (ne_neg : m ≠ -n) : smulX m ≠ smulX n

theorem WeierstrassCurve.Univ.Affine.smulX_eq_smulX_iff {m n : ℤ} : smulX m = smulX n ↔ m = n ∨ m = -n

theorem WeierstrassCurve.Univ.Affine.smulY_sub_negY {n : ℤ} (h0 : n ≠ 0) : smulY n - pointedCurve.toAffine.negY (smulX n) (smulY n) = ψᵤ (2 * n) / ψᵤ n ^ 4

theorem WeierstrassCurve.Univ.Affine.smulY_one_sub_negY : smulY 1 - pointedCurve.toAffine.negY (smulX 1) (smulY 1) = ψᵤ 2

theorem WeierstrassCurve.Univ.Affine.smulY_one_ne_negY : smulY 1 ≠ pointedCurve.toAffine.negY (smulX 1) (smulY 1)

noncomputable def WeierstrassCurve.Univ.Affine.slopeOne : Univ.Field

The tangent slope at the generic point of the universal curve.

Equations

• One or more equations did not get rendered due to their size.

theorem WeierstrassCurve.Univ.Affine.slopeOne_eq_neg_div : slopeOne = -polyToField curve.polynomialX / ψᵤ 2

theorem WeierstrassCurve.Univ.Affine.addX_smul_one_smul_one : pointedCurve.toAffine.addX (smulX 1) (smulX 1) slopeOne = smulX 2

theorem WeierstrassCurve.Univ.Affine.addY_smul_one_smul_one : pointedCurve.toAffine.addY (smulX 1) (smulX 1) (smulY 1) slopeOne = smulY 2

theorem WeierstrassCurve.Univ.Affine.ωe_neg' {n : ℤ} : WeierstrassCurve.ωe curve (-n) = WeierstrassCurve.ωe curve n + Polynomial.CC curve.a₁ * WeierstrassCurve.φ curve n * WeierstrassCurve.ψ curve n + Polynomial.CC curve.a₃ * WeierstrassCurve.ψ curve n ^ 3

theorem WeierstrassCurve.Univ.Affine.smulY_neg {n : ℤ} (h0 : n ≠ 0) : smulY (-n) = pointedCurve.toAffine.negY (smulX n) (smulY n)

theorem WeierstrassCurve.Univ.Affine.smulX_add {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) (add_ne : n + m ≠ 0) (sub_ne : n - m ≠ 0) : have ψ₂ := fun (x y : Univ.Field) => y - pointedCurve.toAffine.negY x y; smulX (n + m) = smulX (n - m) - ψ₂ (smulX n) (smulY n) * ψ₂ (smulX m) (smulY m) / (smulX m - smulX n) ^ 2

theorem WeierstrassCurve.Univ.Affine.smulY_add_sub_negY {m n : ℤ} (hm : m ≠ 0) (hn : n ≠ 0) (add_ne : n + m ≠ 0) (sub_ne : n - m ≠ 0) : have ψ₂ := fun (x y : Univ.Field) => y - pointedCurve.toAffine.negY x y; ψ₂ (smulX (n + m)) (smulY (n + m)) = (ψ₂ (smulX m) (smulY m) * (smulX n - smulX (n + m)) - ψ₂ (smulX n) (smulY n) * (smulX m - smulX (n + m))) / (smulX m - smulX n)

@[instance_reducible]

noncomputable instance WeierstrassCurve.Univ.Affine.instAddGroupPointFieldBaseChangeMvPolynomialCoeffIntCurve : AddGroup (curve.baseChange Univ.Field).Point

Equations

• WeierstrassCurve.Univ.Affine.instAddGroupPointFieldBaseChangeMvPolynomialCoeffIntCurve = inferInstance

theorem WeierstrassCurve.Univ.Affine.zsmul_point_eq_smulX_smulY {n : ℤ} : n ≠ 0 → ∃ (h : Affine.Nonsingular curveField (smulX n) (smulY n)), n • point = Affine.Point.some (smulX n) (smulY n) h

theorem WeierstrassCurve.Univ.Affine.nonsingular_smulX_smulY {n : ℤ} (hn : n ≠ 0) : Affine.Nonsingular curveField (smulX n) (smulY n)

theorem WeierstrassCurve.Univ.Affine.zsmul_point_ne_zero {n : ℤ} (h0 : n ≠ 0) : n • point ≠ 0

theorem WeierstrassCurve.Univ.Jacobian.zsmul_point_ne_zero {n : ℤ} (h0 : n ≠ 0) : n • point ≠ 0

theorem WeierstrassCurve.Univ.Jacobian.zsmul_point_ne {m n : ℤ} (h : m ≠ n) : m • point ≠ n • point

theorem WeierstrassCurve.Univ.Jacobian.point_point : point.point = ⟦![polyToField (Polynomial.C Polynomial.X), polyToField Polynomial.X, 1]⟧

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.Jacobian.smulPoly (n : ℤ) : Fin 3 → Poly

The coordinate-polynomial triple [φₙ, ωₙ, ψₙ] for multiplication by an integer.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.Jacobian.smulRing (n : ℤ) : Fin 3 → Univ.Ring

The multiplication-coordinate triple mapped to the universal coordinate ring.

Equations

• WeierstrassCurve.Univ.Jacobian.smulRing n = ⇑(AdjoinRoot.mk WeierstrassCurve.Univ.curve.polynomial) ∘ WeierstrassCurve.Univ.Jacobian.smulPoly n

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.Univ.Jacobian.smulField (n : ℤ) : Fin 3 → Univ.Field

The multiplication-coordinate triple mapped to the universal function field.

Equations

• WeierstrassCurve.Univ.Jacobian.smulField n = ⇑WeierstrassCurve.Univ.polyToField ∘ WeierstrassCurve.Univ.Jacobian.smulPoly n

theorem WeierstrassCurve.Univ.Jacobian.algebraMap_comp_smulRing (n : ℤ) : ⇑(algebraMap Univ.Ring Univ.Field) ∘ smulRing n = smulField n

theorem WeierstrassCurve.Univ.Jacobian.zsmul_point_eq_smulField {n : ℤ} : (n • point).point = ⟦smulField n⟧

theorem WeierstrassCurve.Univ.Jacobian.dblZ_smulPoly {n : ℤ} : Jacobian.dblZ curvePoly (smulPoly n) = WeierstrassCurve.ψ curve (2 * n)

theorem WeierstrassCurve.Univ.Jacobian.nonsingular_smulField {n : ℤ} : Jacobian.Nonsingular curveField (smulField n)

theorem WeierstrassCurve.Univ.Jacobian.dblXYZ_smulField {n : ℤ} : Jacobian.dblXYZ curveField (smulField n) = smulField (2 * n)

theorem WeierstrassCurve.Univ.Jacobian.dblXYZ_smulRing {n : ℤ} : Jacobian.dblXYZ curveRing (smulRing n) = smulRing (2 * n)

theorem WeierstrassCurve.Univ.Jacobian.addZ_smulPoly {m n : ℤ} : Jacobian.addZ (smulPoly m) (smulPoly n) = WeierstrassCurve.ψ curve (n + m) * WeierstrassCurve.ψ curve (n - m)

theorem WeierstrassCurve.Univ.Jacobian.ωe_neg_eq_neg_negY {n : ℤ} : WeierstrassCurve.ωe curve (-n) = -Jacobian.negY curvePoly (smulPoly n)

theorem WeierstrassCurve.Univ.Jacobian.smulPoly_neg {n : ℤ} : smulPoly (-n) = -1 • Jacobian.neg curvePoly (smulPoly n)

theorem WeierstrassCurve.Univ.Jacobian.smulRing_neg {n : ℤ} : smulRing (-n) = -1 • Jacobian.neg curveRing (smulRing n)

theorem WeierstrassCurve.Univ.Jacobian.smulField_neg {n : ℤ} : smulField (-n) = -1 • Jacobian.neg curveField (smulField n)

theorem WeierstrassCurve.Univ.Jacobian.smulPoly_zero : smulPoly 0 = ![1, 1, 0]

theorem WeierstrassCurve.Univ.Jacobian.smulField_zero : smulField 0 = ![1, 1, 0]

theorem WeierstrassCurve.Univ.Jacobian.addXYZ_smulField {m n : ℤ} : Jacobian.addXYZ curveField (smulField m) (smulField n) = polyToField (WeierstrassCurve.ψ curve (n - m)) • smulField (n + m)

theorem WeierstrassCurve.Univ.Jacobian.addXYZ_smulRing {m n : ℤ} : Jacobian.addXYZ curveRing (smulRing m) (smulRing n) = (AdjoinRoot.mk curve.polynomial) (WeierstrassCurve.ψ curve (n - m)) • smulRing (n + m)

theorem WeierstrassCurve.Univ.Jacobian.addXYZ_smulField₁ {n : ℤ} : Jacobian.addXYZ curveField (smulField n) (smulField (n + 1)) = smulField (2 * n + 1)

theorem WeierstrassCurve.Univ.Jacobian.addXYZ_smulRing₁ {n : ℤ} : Jacobian.addXYZ curveRing (smulRing n) (smulRing (n + 1)) = smulRing (2 * n + 1)

@[reducible, inline]

noncomputable abbrev WeierstrassCurve.smulEval {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) (x y : R) (n : ℤ) : Fin 3 → R

Evaluate the multiplication-coordinate triple at the given affine coordinates.

Equations

• W.smulEval x y n = Polynomial.evalEval x y ∘ ![W.φ n, W.ωe n, W.ψ n]

theorem WeierstrassCurve.ringEval_comp_smulRing {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : W.toAffine.Equation x y) (n : ℤ) : ⇑(Univ.ringEval eqn) ∘ Univ.Jacobian.smulRing n = W.smulEval x y n

theorem WeierstrassCurve.ringEval_ψ {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : W.toAffine.Equation x y) (n : ℤ) : (Univ.ringEval eqn) ((AdjoinRoot.mk Univ.curve.polynomial) (WeierstrassCurve.ψ Univ.curve n)) = Polynomial.evalEval x y (W.ψ n)

theorem WeierstrassCurve.dblXYZ_smulEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : W.toAffine.Equation x y) (n : ℤ) : Jacobian.dblXYZ W (W.smulEval x y n) = W.smulEval x y (2 * n)

theorem WeierstrassCurve.addXYZ_smulEval {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : W.toAffine.Equation x y) (m n : ℤ) : Jacobian.addXYZ W (W.smulEval x y m) (W.smulEval x y n) = Polynomial.evalEval x y (W.ψ (n - m)) • W.smulEval x y (n + m)

theorem WeierstrassCurve.addXYZ_smulEval₁ {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} {x y : R} (eqn : W.toAffine.Equation x y) (n : ℤ) : Jacobian.addXYZ W (W.smulEval x y n) (W.smulEval x y (n + 1)) = W.smulEval x y (2 * n + 1)

theorem WeierstrassCurve.zsmul_eq_smulEval {F : Type u_3} [Field F] (W : WeierstrassCurve F) {x y : F} (h : Affine.Nonsingular W x y) (n : ℤ) : (n • Jacobian.Point.fromAffine (Affine.Point.some x y h)).point = ⟦W.smulEval x y n⟧

theorem WeierstrassCurve.evalEval_ψ_sq {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (h : W.toAffine.Equation x y) (n : ℤ) : Polynomial.evalEval x y (W.ψ n) ^ 2 = Polynomial.eval x (W.ΨSq n)

theorem WeierstrassCurve.evalEval_φ {F : Type u_1} [Field F] (W : WeierstrassCurve F) {x y : F} (h : W.toAffine.Equation x y) (n : ℤ) : Polynomial.evalEval x y (W.φ n) = Polynomial.eval x (W.Φ n)

theorem WeierstrassCurve.smul_eq_zero_iff_evalEval_ψ {F : Type u_1} [Field F] [DecidableEq F] (W : WeierstrassCurve F) {x y : F} (h : W.toAffine.Nonsingular x y) (n : ℤ) : n • Affine.Point.some x y h = 0 ↔ Polynomial.evalEval x y (W.ψ n) = 0