LeanPool.EcTateLean.Algebra.EllipticCurve.Model

Imported Lean Pool material for LeanPool.EcTateLean.Algebra.EllipticCurve.Model.

structure Model (R : Type u) [CommRing R] : Type u

A model of a (possibly singular) elliptic curve is given by a invariants $$a₁, a₂, a₃, a₄, a₆$$ which represent the curve $$ y^2 + a₁ xy + a₃ y = x^ 3 + a₂ x ^ 2 + a₄ x + a₆ $$

• a1 : R

  The a₁ coefficient of the Weierstrass model.

• a2 : R

  The a₂ coefficient of the Weierstrass model.

• a3 : R

  The a₃ coefficient of the Weierstrass model.

• a4 : R

  The a₄ coefficient of the Weierstrass model.

• a6 : R

  The a₆ coefficient of the Weierstrass model.

@[implicit_reducible]

instance instInhabitedModel {a✝ : Type u_1} [Inhabited a✝] {a✝¹ : CommRing a✝} : Inhabited (Model a✝)

Equations

• instInhabitedModel = { default := instInhabitedModel.default }

def instDecidableEqModel.decEq {R✝ : Type u_1} {inst✝ : CommRing R✝} [DecidableEq R✝] (x✝ x✝¹ : Model R✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqModel {R✝ : Type u_1} {inst✝ : CommRing R✝} [DecidableEq R✝] : DecidableEq (Model R✝)

Equations

• instDecidableEqModel = instDecidableEqModel.decEq

@[implicit_reducible]

instance Model.instRepr {R : Type u} [CommRing R] [Repr R] : Repr (Model R)

Equations

• Model.instRepr = { reprPrec := fun (e : Model R) (x : ℕ) => repr (e.a1, e.a2, e.a3, e.a4, e.a6) }

def Model.b2 {R : Type u} [CommRing R] (e : Model R) : R

The b₂ invariant of a Weierstrass model.

Equations

• e.b2 = e.a1 * e.a1 + 4 * e.a2

def Model.b4 {R : Type u} [CommRing R] (e : Model R) : R

The b₄ invariant of a Weierstrass model.

Equations

• e.b4 = e.a1 * e.a3 + 2 * e.a4

def Model.b6 {R : Type u} [CommRing R] (e : Model R) : R

The b₆ invariant of a Weierstrass model.

Equations

• e.b6 = e.a3 * e.a3 + 4 * e.a6

def Model.b8 {R : Type u} [CommRing R] (e : Model R) : R

The b₈ invariant of a Weierstrass model.

Equations

• e.b8 = e.a1 * e.a1 * e.a6 - e.a1 * e.a3 * e.a4 + 4 * e.a2 * e.a6 + e.a2 * e.a3 * e.a3 - e.a4 * e.a4

def Model.b5 {R : Type u} [CommRing R] (e : Model R) : R

The b₅ invariant of a Weierstrass model (from Connell).

Equations

• e.b5 = e.a1 * e.a4 - 2 * e.a2 * e.a3

def Model.b7 {R : Type u} [CommRing R] (e : Model R) : R

The b₇ invariant of a Weierstrass model (from Connell).

Equations

• e.b7 = e.a1 * (e.a3 ^ 2 - 12 * e.a6) + 8 * e.a3 * e.a4

theorem Model.b8_identity {R : Type u} [CommRing R] (e : Model R) : 4 * e.b8 = e.b2 * e.b6 - e.b4 ^ 2

def Model.c4 {R : Type u} [CommRing R] (e : Model R) : R

The c₄ invariant of a Weierstrass model.

Equations

• e.c4 = e.b2 ^ 2 - 24 * e.b4

def Model.c6 {R : Type u} [CommRing R] (e : Model R) : R

The c₆ invariant of a Weierstrass model.

Equations

• e.c6 = -e.b2 ^ 3 + 36 * e.b2 * e.b4 - 216 * e.b6

def Model.discr {R : Type u} [CommRing R] (e : Model R) : R

The discriminant of a Weierstrass model.

Equations

• e.discr = -e.b2 * e.b2 * e.b8 - 8 * e.b4 ^ 3 - 27 * e.b6 * e.b6 + 9 * e.b2 * e.b4 * e.b6

theorem Model.discr_identity {R : Type u} [CommRing R] (e : Model R) : 1728 * e.discr = e.c4 ^ 3 - e.c6 ^ 2

structure Model.urstTransform (R : Type u_1) [Ring R] : Type u_1

A change of coordinates (u, r, s, t) of a Weierstrass model, with u a unit and r, s, t ring elements.

• u : Rˣ

  The scaling unit of the change of coordinates.

• r : R

  The x-translation of the change of coordinates.

• s : R

  The xy-shear of the change of coordinates.

• t : R

  The y-translation of the change of coordinates.

@[implicit_reducible]

instance Model.urstTransform.instMulURSTTransform {R : Type u} [CommRing R] : Mul (urstTransform R)

Equations

• Model.urstTransform.instMulURSTTransform = { mul := fun (f g : Model.urstTransform R) => { u := f.u * g.u, r := f.r + ↑f.u * g.r, s := f.s + ↑f.u * g.s, t := f.t + ↑f.u * g.t } }

theorem Model.urstTransform.mul_def {R : Type u} [CommRing R] (f g : urstTransform R) : f * g = { u := f.u * g.u, r := f.r + ↑f.u * g.r, s := f.s + ↑f.u * g.s, t := f.t + ↑f.u * g.t }

@[implicit_reducible]

instance Model.urstTransform.instOne {R : Type u} [CommRing R] : One (urstTransform R)

Equations

• Model.urstTransform.instOne = { one := { u := 1, r := 0, s := 0, t := 0 } }

theorem Model.urstTransform.one_def {R : Type u} [CommRing R] : 1 = { u := 1, r := 0, s := 0, t := 0 }

@[implicit_reducible]

instance Model.urstTransform.instMonoid {R : Type u} [CommRing R] : Monoid (urstTransform R)

Equations

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

@[implicit_reducible]

instance Model.urstTransform.instInv {R : Type u} [CommRing R] : Inv (urstTransform R)

Equations

• Model.urstTransform.instInv = { inv := fun (f : Model.urstTransform R) => { u := f.u⁻¹, r := -↑f.u⁻¹ * f.r, s := -↑f.u⁻¹ * f.s, t := -↑f.u⁻¹ * f.t } }

theorem Model.urstTransform.inv_def {R : Type u} [CommRing R] (f : urstTransform R) : f⁻¹ = { u := f.u⁻¹, r := -↑f.u⁻¹ * f.r, s := -↑f.u⁻¹ * f.s, t := -↑f.u⁻¹ * f.t }

@[implicit_reducible]

instance Model.urstTransform.instGroup {R : Type u} [CommRing R] : Group (urstTransform R)

Equations

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

def Model.rstTransform {R : Type u} [CommRing R] : Type u

The change-of-coordinates transformations with trivial scaling unit u = 1.

Equations

• Model.rstTransform = { urst : Model.urstTransform R // urst.u = 1 }

def Model.rstIso {R : Type u} [CommRing R] (r s t : R) (e : Model R) : Model R

The Weierstrass model obtained from e by the change of coordinates (1, r, s, t).

Equations

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

theorem Model.rst_b2 {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).b2 = e.b2 + 12 * r

theorem Model.rst_b4 {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).b4 = e.b4 + r * (e.b2 + 6 * r)

theorem Model.rst_b6 {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).b6 = e.b6 + 2 * r * e.b4 + r * r * e.b2 + 4 * r * r * r

theorem Model.rst_b8 {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).b8 = e.b8 + 3 * r * e.b6 + 3 * r * r * e.b4 + r * r * r * e.b2 + 3 * r * r * r * r

@[simp]

theorem Model.rst_c4 {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).c4 = e.c4

@[simp]

theorem Model.rst_c6 {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).c6 = e.c6

theorem Model.rst_discr {R : Type u} [CommRing R] (r s t : R) (e : Model R) : (rstIso r s t e).discr = e.discr

def Model.map {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) : Model R → Model S

Pushes a Weierstrass model forward along a ring homomorphism f.

Equations

• Model.map f e = { a1 := f e.a1, a2 := f e.a2, a3 := f e.a3, a4 := f e.a4, a6 := f e.a6 }

@[simp]

theorem Model.map_a3 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (a✝ : Model R) : (map f a✝).a3 = f a✝.a3

@[simp]

theorem Model.map_a1 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (a✝ : Model R) : (map f a✝).a1 = f a✝.a1

@[simp]

theorem Model.map_a4 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (a✝ : Model R) : (map f a✝).a4 = f a✝.a4

@[simp]

theorem Model.map_a6 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (a✝ : Model R) : (map f a✝).a6 = f a✝.a6

@[simp]

theorem Model.map_a2 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (a✝ : Model R) : (map f a✝).a2 = f a✝.a2

@[simp]

theorem Model.map_b2 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).b2 = f e.b2

@[simp]

theorem Model.map_b4 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).b4 = f e.b4

@[simp]

theorem Model.map_b5 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).b5 = f e.b5

@[simp]

theorem Model.map_b6 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).b6 = f e.b6

@[simp]

theorem Model.map_b7 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).b7 = f e.b7

@[simp]

theorem Model.map_b8 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).b8 = f e.b8

@[simp]

theorem Model.map_c4 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).c4 = f e.c4

@[simp]

theorem Model.map_c6 {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).c6 = f e.c6

@[simp]

theorem Model.map_discr {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) {e : Model R} : (map f e).discr = f e.discr

def Model.weierstrass {R : Type u} [CommRing R] (e : Model R) (P : R × R) : R

The Weierstrass polynomial of e evaluated at a point P = (x, y), i.e. the difference of the two sides of the Weierstrass equation.

Equations

• e.weierstrass P = P.2 ^ 2 + e.a1 * P.1 * P.2 + e.a3 * P.2 - (P.1 ^ 3 + e.a2 * P.1 ^ 2 + e.a4 * P.1 + e.a6)

def Model.dweierstrassDx {R : Type u} [CommRing R] (e : Model R) (P : R × R) : R

The partial derivative of the Weierstrass polynomial with respect to x, evaluated at P.

Equations

• e.dweierstrassDx P = e.a1 * P.2 - (3 * P.1 ^ 2 + 2 * e.a2 * P.1 + e.a4)

def Model.dweierstrassDy {R : Type u} [CommRing R] (e : Model R) (P : R × R) : R

The partial derivative of the Weierstrass polynomial with respect to y, evaluated at P.

Equations

• e.dweierstrassDy P = 2 * P.2 + e.a1 * P.1 + e.a3

@[simp]

theorem Model.weierstrass_map {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (e : Model R) (P : R × R) : (map f e).weierstrass (Prod.map (⇑f) (⇑f) P) = f (e.weierstrass P)

@[simp]

theorem Model.dweierstrassDx_map {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (e : Model R) (P : R × R) : (map f e).dweierstrassDx (Prod.map (⇑f) (⇑f) P) = f (e.dweierstrassDx P)

@[simp]

theorem Model.dweierstrassDy_map {R : Type u} [CommRing R] {S : Type u} [CommRing S] (f : R →+* S) (e : Model R) (P : R × R) : (map f e).dweierstrassDy (Prod.map (⇑f) (⇑f) P) = f (e.dweierstrassDy P)

theorem Model.discr_eq_neg_singular {R : Type u} [CommRing R] (e : Model R) : e.discr = -(e.a1 ^ 4 * e.a2 * e.a3 ^ 2 - e.a1 ^ 5 * e.a3 * e.a4 + e.a1 ^ 6 * e.a6 + 8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 ^ 2 - e.a1 ^ 3 * e.a3 ^ 3 - 8 * e.a1 ^ 3 * e.a2 * e.a3 * e.a4 - e.a1 ^ 4 * e.a4 ^ 2 + 12 * e.a1 ^ 4 * e.a2 * e.a6 + 16 * e.a2 ^ 3 * e.a3 ^ 2 - 36 * e.a1 * e.a2 * e.a3 ^ 3 - 16 * e.a1 * e.a2 ^ 2 * e.a3 * e.a4 + 30 * e.a1 ^ 2 * e.a3 ^ 2 * e.a4 - 8 * e.a1 ^ 2 * e.a2 * e.a4 ^ 2 + 48 * e.a1 ^ 2 * e.a2 ^ 2 * e.a6 - 36 * e.a1 ^ 3 * e.a3 * e.a6 + 27 * e.a3 ^ 4 - 72 * e.a2 * e.a3 ^ 2 * e.a4 - 16 * e.a2 ^ 2 * e.a4 ^ 2 + 96 * e.a1 * e.a3 * e.a4 ^ 2 + 64 * e.a2 ^ 3 * e.a6 - 144 * e.a1 * e.a2 * e.a3 * e.a6 - 72 * e.a1 ^ 2 * e.a4 * e.a6 + 64 * e.a4 ^ 3 + 216 * e.a3 ^ 2 * e.a6 - 288 * e.a2 * e.a4 * e.a6 + 432 * e.a6 ^ 2)

The discriminant equals (minus) the standard order-a6 generator of the elimination ideal of the Weierstrass and partial-derivative polynomials. This identity (verified with Singular.jl, part of OSCAR) is the negative of the a6-resultant polynomial below.

theorem Model.discr_in_jacobian_ideal {R : Type u} [CommRing R] (e : Model R) (P : R × R) : e.discr = -((48 * P.1 * P.2 * e.a2 ^ 2 + 24 * e.a1 * e.a2 * e.a6 + 216 * P.2 * e.a6 + P.2 * e.a1 ^ 6 + 11 * P.2 * e.a1 ^ 4 * e.a2 + P.1 * e.a1 ^ 4 * e.a3 + 38 * P.1 * e.a1 ^ 2 * e.a2 * e.a3 + 8 * e.a1 ^ 2 * e.a2 ^ 2 * e.a3 + e.a1 ^ 4 * e.a2 * e.a3 + 40 * P.2 * e.a1 ^ 2 * e.a2 ^ 2 + 32 * P.2 * e.a2 ^ 3 + 24 * P.1 * P.2 * e.a1 * e.a3 + 30 * P.1 ^ 2 * e.a2 * e.a3 + 3 * P.1 * e.a1 ^ 3 * e.a4 + 60 * P.1 ^ 2 * e.a1 * e.a4 + 30 * P.1 ^ 2 * e.a1 ^ 2 * e.a3 + 31 * e.a1 ^ 2 * e.a3 * e.a4 + 144 * P.2 ^ 2 * e.a3 + 198 * P.2 * e.a3 ^ 2 + 27 * e.a3 ^ 3 + 60 * e.a1 * e.a4 ^ 2 + 36 * P.1 * e.a1 * e.a6 + 76 * P.1 * e.a2 ^ 2 * e.a3 + 16 * e.a2 ^ 3 * e.a3 + 84 * P.1 * e.a1 * e.a2 * e.a4 - (36 * e.a3 * e.a6 + P.1 ^ 2 * e.a1 ^ 5 + P.1 * e.a1 ^ 5 * e.a2 + P.1 * P.2 * e.a1 ^ 4 + 9 * P.1 ^ 2 * e.a1 ^ 3 * e.a2 + 10 * P.1 * e.a1 ^ 3 * e.a2 ^ 2 + e.a1 ^ 5 * e.a4 + 6 * P.2 ^ 2 * e.a1 ^ 3 + 8 * P.1 * P.2 * e.a1 ^ 2 * e.a2 + 24 * P.1 ^ 2 * e.a1 * e.a2 ^ 2 + 32 * P.1 * e.a1 * e.a2 ^ 3 + 35 * P.2 * e.a1 ^ 3 * e.a3 + e.a1 ^ 3 * e.a3 ^ 2 + 9 * e.a1 ^ 3 * e.a2 * e.a4 + 48 * P.2 ^ 2 * e.a1 * e.a2 + 134 * P.2 * e.a1 * e.a2 * e.a3 + 27 * P.1 * e.a1 * e.a3 ^ 2 + 36 * e.a1 * e.a2 * e.a3 ^ 2 + 58 * P.2 * e.a1 ^ 2 * e.a4 + 24 * e.a1 * e.a2 ^ 2 * e.a4 + 144 * P.1 * P.2 * e.a4 + 120 * P.2 * e.a2 * e.a4 + 168 * P.1 * e.a3 * e.a4 + 34 * e.a2 * e.a3 * e.a4)) * e.dweierstrassDy P + (e.a1 ^ 2 * e.a3 ^ 2 + 12 * e.a1 ^ 2 * e.a6 + 16 * e.a2 ^ 2 * e.a4 + 32 * P.1 * e.a2 ^ 3 + e.a1 ^ 4 * e.a4 + 144 * P.1 * e.a6 + 48 * e.a2 * e.a6 + P.1 * e.a1 ^ 4 * e.a2 + 84 * P.1 * e.a3 ^ 2 + 56 * P.2 * e.a1 * e.a4 + 8 * e.a1 ^ 2 * e.a2 * e.a4 + 28 * P.2 * e.a1 ^ 2 * e.a3 + 52 * P.2 * e.a2 * e.a3 + 96 * P.1 * P.2 * e.a3 + 8 * P.1 * e.a1 ^ 2 * e.a2 ^ 2 + 38 * e.a2 * e.a3 ^ 2 + 32 * P.1 ^ 2 * e.a2 ^ 2 - (2 * P.1 * e.a1 ^ 3 * e.a3 + 112 * P.1 * e.a2 * e.a4 + e.a1 ^ 3 * e.a2 * e.a3 + 36 * e.a1 * e.a3 * e.a4 + 96 * P.1 ^ 2 * e.a4 + 32 * P.1 * P.2 * e.a1 * e.a2 + 32 * P.2 * e.a1 * e.a2 ^ 2 + 64 * e.a4 ^ 2 + 4 * P.1 * P.2 * e.a1 ^ 3 + 10 * P.2 * e.a1 ^ 3 * e.a2 + P.2 * e.a1 ^ 5 + 8 * e.a1 * e.a2 ^ 2 * e.a3 + 46 * P.1 * e.a1 * e.a2 * e.a3)) * e.dweierstrassDx P + (60 * e.a1 ^ 2 * e.a4 + 288 * P.1 * e.a4 + 240 * e.a2 * e.a4 + 12 * P.2 * e.a1 ^ 3 + 36 * e.a1 ^ 3 * e.a3 + 96 * P.2 * e.a1 * e.a2 + 168 * e.a1 * e.a2 * e.a3 - (432 * e.a6 + e.a1 ^ 6 + 288 * P.2 * e.a3 + 252 * e.a3 ^ 2 + 12 * e.a1 ^ 4 * e.a2 + 48 * e.a1 ^ 2 * e.a2 ^ 2 + 96 * P.1 * e.a2 ^ 2 + 64 * e.a2 ^ 3)) * e.weierstrass P)

def Model.varChange {R : Type u} [CommRing R] (r s t : R) (P' : R × R) : R × R

The change of variables on points induced by the change of coordinates (1, r, s, t).

Equations

• Model.varChange r s t P' = (P'.1 + r, P'.2 + s * P'.1 + t)

@[simp]

theorem Model.varChange_comp {R : Type u} [CommRing R] (r s t r' s' t' : R) (P : R × R) : varChange r s t (varChange r' s' t' P) = varChange (r + r') (s + s') (t + t' + s * r') P

@[simp]

theorem Model.varChange_zero {R : Type u} [CommRing R] (P : R × R) : varChange 0 0 0 P = P

theorem Model.weierstrass_iso_eq_varChange {R : Type u} [CommRing R] {r s t : R} (e : Model R) (P : R × R) : (rstIso r s t e).weierstrass P = e.weierstrass (varChange r s t P)

theorem Model.dweierstrassDx_iso_eq_varChange {R : Type u} [CommRing R] {r s t : R} (e : Model R) (P : R × R) : (rstIso r s t e).dweierstrassDx P = e.dweierstrassDx (varChange r s t P) + s * e.dweierstrassDy (varChange r s t P)

theorem Model.dweierstrassDy_iso_eq_varChange {R : Type u} [CommRing R] {r s t : R} (e : Model R) (P : R × R) : (rstIso r s t e).dweierstrassDy P = e.dweierstrassDy (varChange r s t P)

def Model.rstTriple {R : Type u} [CommRing R] (e : Model R) (rst : R × R × R) : Model R

The change of coordinates (1, r, s, t) applied to e, with the triple rst = (r, s, t) packaged as a single argument.

Equations

• e.rstTriple rst = Model.rstIso rst.1 rst.2.1 rst.2.2 e

theorem Model.rstIso_to_triple {R : Type u} [CommRing R] (e : Model R) (r s t : R) : rstIso r s t e = e.rstTriple (r, s, t)

structure ValidModel (R : Type u) [CommRing R] extends Model R : Type u

A Weierstrass model with nonzero discriminant, i.e. a nonsingular elliptic curve.

• a1 : R
• a2 : R
• a3 : R
• a4 : R
• a6 : R
• discr_not_zero : self.discr ≠ 0

  The discriminant of the underlying model is nonzero.

@[implicit_reducible]

instance ValidModel.instRepr {R : Type u} [CommRing R] [Repr R] : Repr (ValidModel R)

Equations

• ValidModel.instRepr = { reprPrec := fun (e : ValidModel R) (x : ℕ) => repr e.toModel }

def ValidModel.rstIso {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : ValidModel R

The valid model obtained from e by the change of coordinates (1, r, s, t).

Equations

• ValidModel.rstIso r s t e = { toModel := Model.rstIso r s t e.toModel, discr_not_zero := ⋯ }

@[simp]

theorem ValidModel.rstIso_a3 {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : (rstIso r s t e).a3 = e.a3 + r * e.a1 + 2 * t

@[simp]

theorem ValidModel.rstIso_a6 {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : (rstIso r s t e).a6 = e.a6 + r * e.a4 + r * r * e.a2 + r * r * r - t * (e.a3 + t + r * e.a1)

@[simp]

theorem ValidModel.rstIso_a1 {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : (rstIso r s t e).a1 = e.a1 + 2 * s

@[simp]

theorem ValidModel.rstIso_a4 {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : (rstIso r s t e).a4 = e.a4 - s * e.a3 + 2 * r * e.a2 - (t + r * s) * e.a1 + 3 * r * r - 2 * s * t

@[simp]

theorem ValidModel.rstIso_a2 {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : (rstIso r s t e).a2 = e.a2 - s * e.a1 + 3 * r - s * s

@[simp]

theorem ValidModel.rst_discr_valid {R : Type u} [CommRing R] (r s t : R) (e : ValidModel R) : (rstIso r s t e).discr = e.discr

theorem ValidModel.rt_of_a1 {R : Type u} [CommRing R] (e : ValidModel R) (r t : R) : (rstIso r 0 t e).a1 = e.a1

theorem ValidModel.t_of_a2 {R : Type u} [CommRing R] (e : ValidModel R) (t : R) : (rstIso 0 0 t e).a2 = e.a2

theorem ValidModel.r_of_a2 {R : Type u} [CommRing R] (e : ValidModel R) (r : R) : (rstIso r 0 0 e).a2 = e.a2 + 3 * r

theorem ValidModel.t_of_a3 {R : Type u} [CommRing R] (e : ValidModel R) (t : R) : (rstIso 0 0 t e).a3 = e.a3 + 2 * t

theorem ValidModel.r_of_a3 {R : Type u} [CommRing R] (e : ValidModel R) (r : R) : (rstIso r 0 0 e).a3 = e.a3 + r * e.a1

theorem ValidModel.t_of_a4 {R : Type u} [CommRing R] (e : ValidModel R) (t : R) : (rstIso 0 0 t e).a4 = e.a4 - t * e.a1

theorem ValidModel.r_of_a4 {R : Type u} [CommRing R] (e : ValidModel R) (r : R) : (rstIso r 0 0 e).a4 = e.a4 + 2 * r * e.a2 + 3 * r ^ 2

theorem ValidModel.t_of_a6 {R : Type u} [CommRing R] (e : ValidModel R) (t : R) : (rstIso 0 0 t e).a6 = e.a6 - t * e.a3 - t ^ 2

theorem ValidModel.r_of_a6 {R : Type u} [CommRing R] (e : ValidModel R) (r : R) : (rstIso r 0 0 e).a6 = e.a6 + r * e.a4 + r ^ 2 * e.a2 + r ^ 3

theorem ValidModel.st_of_a1 {R : Type u} [CommRing R] (e : ValidModel R) (s t : R) : (rstIso 0 s t e).a1 = e.a1 + 2 * s

theorem ValidModel.st_of_a2 {R : Type u} [CommRing R] (e : ValidModel R) (s t : R) : (rstIso 0 s t e).a2 = e.a2 - s * e.a1 - s ^ 2

theorem ValidModel.st_of_a3 {R : Type u} [CommRing R] (e : ValidModel R) (s t : R) : (rstIso 0 s t e).a3 = e.a3 + 2 * t

theorem ValidModel.st_of_a4 {R : Type u} [CommRing R] (e : ValidModel R) (s t : R) : (rstIso 0 s t e).a4 = e.a4 - s * e.a3 - t * e.a1 - 2 * s * t

theorem ValidModel.st_of_a6 {R : Type u} [CommRing R] (e : ValidModel R) (s t : R) : (rstIso 0 s t e).a6 = e.a6 - t * e.a3 - t ^ 2

theorem ValidModel.st_of_b8 {R : Type u} [CommRing R] (e : ValidModel R) (s t : R) : (rstIso 0 s t e).b8 = e.b8

def ValidModel.rstTriple {R : Type u} [CommRing R] (e : ValidModel R) (rst : R × R × R) : ValidModel R

The change of coordinates (1, r, s, t) applied to the valid model e, with the triple rst = (r, s, t) packaged as a single argument.

Equations

• e.rstTriple rst = ValidModel.rstIso rst.1 rst.2.1 rst.2.2 e

theorem ValidModel.rstIso_to_triple {R : Type u} [CommRing R] (e : ValidModel R) (r s t : R) : rstIso r s t e = e.rstTriple (r, s, t)

def Model.isSingularPoint {K : Type u} [CommRing K] (e : Model K) (P : K × K) : Prop

A point P is a singular point of the model e when the Weierstrass polynomial and both of its partial derivatives vanish at P.

Equations

• e.isSingularPoint P = (e.weierstrass P = 0 ∧ e.dweierstrassDx P = 0 ∧ e.dweierstrassDy P = 0)

theorem Model.discr_eq_zero_of_singular {K : Type u} [CommRing K] (e : Model K) {P : K × K} (h : e.isSingularPoint P) : e.discr = 0

theorem Model.c4_zero_iff_a1_zero_of_char_two {K : Type u} [CommRing K] [IsDomain K] (e : Model K) (h : ringChar K = 2) : e.c4 = 0 ↔ e.a1 = 0

theorem Model.c4_zero_iff_b2_zero_of_char_three {K : Type u} [CommRing K] [IsDomain K] (e : Model K) (h : ringChar K = 3) : e.c4 = 0 ↔ e.b2 = 0

theorem Model.a3_zero_of_a1_zero_of_disc_zero_of_char_two {K : Type u} [CommRing K] [IsDomain K] (e : Model K) (h : ringChar K = 2) (hdisc : e.discr = 0) (ha1 : e.a1 = 0) : e.a3 = 0

theorem Model.b4_zero_of_b2_zero_of_disc_zero_of_char_three {K : Type u} [CommRing K] [IsDomain K] (e : Model K) (h : ringChar K = 3) (hdisc : e.discr = 0) (hb2 : e.b2 = 0) : e.b4 = 0

noncomputable def Model.Field.singularPoint {K : Type u} [Field K] [ECTate.PerfectRing K] (e : Model K) : K × K

Proposition 1.5.4 of Elliptic Curve Handbook, Ian Connell February, 1999, https://www.math.rug.nl/~top/ian.pdf

Equations

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

theorem Model.Field.ringChar_eq_of_Prime {K : Type u} [Field K] {n : ℕ} [n.AtLeastTwo] (hn : OfNat.ofNat n = 0) (hnp : Nat.Prime n) : ringChar K = n

theorem Model.Field.isSingularPoint_singularPoint {K : Type u} [Field K] [ECTate.PerfectRing K] (e : Model K) (h : e.discr = 0) : e.isSingularPoint (singularPoint e)

noncomputable def Model.Field.moveSingularPointToOriginTriple {K : Type u} [Field K] [ECTate.PerfectRing K] (e : Model K) : K × K × K

Proposition 1.5.4 of Elliptic Curve Handbook, Ian Connell February, 1999, https://www.math.rug.nl/~top/ian.pdf

Equations

• Model.Field.moveSingularPointToOriginTriple e = ((Model.Field.singularPoint e).1, 0, (Model.Field.singularPoint e).2)

noncomputable def Model.Field.moveSingularPointToOriginIso {K : Type u} [Field K] [ECTate.PerfectRing K] (e : Model K) : Model K

The model obtained from e by the change of coordinates that moves its singular point to the origin.

Equations

• Model.Field.moveSingularPointToOriginIso e = e.rstTriple (Model.Field.moveSingularPointToOriginTriple e)

theorem Model.Field.move_singularPoint {K : Type u} [Field K] (e : Model K) (r t : K) {P : K × K} (h : e.isSingularPoint P) : (rstIso r 0 t e).isSingularPoint (varChange (-r) 0 (-t) P)

theorem Model.Field.move_singularPoint_to_origin {K : Type u} [Field K] [ECTate.PerfectRing K] (e : Model K) (h : e.discr = 0) : (moveSingularPointToOriginIso e).isSingularPoint (0, 0)

theorem Model.Field.move_singularPoint_to_origin' {K : Type u} [Field K] [ECTate.PerfectRing K] (e : Model K) : (∃ (P : K × K), e.isSingularPoint P) → (moveSingularPointToOriginIso e).isSingularPoint (0, 0)