Some normal forms of elliptic curves

This file defines some normal forms of Weierstrass equations of elliptic curves.

Main definitions and results

The following normal forms are in [Sil09], section III.1, page 42.

• WeierstrassCurve.IsCharNeTwoNF is a type class which asserts that a WeierstrassCurve is of form $Y^2 = X^3 + a_2X^2 + a_4X + a_6$. It is the normal form of characteristic ≠ 2.

  If 2 is invertible in the ring (for example, if it is a field of characteristic ≠ 2), then for any WeierstrassCurve there exists a change of variables which will change it into such normal form (WeierstrassCurve.exists_variableChange_isCharNeTwoNF). See also WeierstrassCurve.toCharNeTwoNF and WeierstrassCurve.toCharNeTwoNF_spec.

The following normal forms are in [Sil09], Appendix A, Proposition 1.1.

• WeierstrassCurve.IsShortNF is a type class which asserts that a WeierstrassCurve is of form $Y^2 = X^3 + a_4X + a_6$. It is the normal form of characteristic ≠ 2 or 3, and also the normal form of characteristic = 3 and j = 0.

  If 2 and 3 are invertible in the ring (for example, if it is a field of characteristic ≠ 2 or 3), then for any WeierstrassCurve there exists a change of variables which will change it into such normal form (WeierstrassCurve.exists_variableChange_isShortNF). See also WeierstrassCurve.toShortNF and WeierstrassCurve.toShortNF_spec.

  If the ring is of characteristic = 3, then for any WeierstrassCurve with $b_2 = 0$ (for an elliptic curve, this is equivalent to j = 0), there exists a change of variables which will change it into such normal form (see WeierstrassCurve.toShortNFOfCharThree and WeierstrassCurve.toShortNFOfCharThree_spec).

• WeierstrassCurve.IsCharThreeJNeZeroNF is a type class which asserts that a WeierstrassCurve is of form $Y^2 = X^3 + a_2X^2 + a_6$. It is the normal form of characteristic = 3 and j ≠ 0.

  If the field is of characteristic = 3, then for any WeierstrassCurve with $b_2 \neq 0$ (for an elliptic curve, this is equivalent to j ≠ 0), there exists a change of variables which will change it into such normal form (see WeierstrassCurve.toCharThreeNF and WeierstrassCurve.toCharThreeNF_spec_of_b₂_ne_zero).

• WeierstrassCurve.IsCharThreeNF is the combination of the above two, that is, asserts that a WeierstrassCurve is of form $Y^2 = X^3 + a_2X^2 + a_6$ or $Y^2 = X^3 + a_4X + a_6$. It is the normal form of characteristic = 3.

  If the field is of characteristic = 3, then for any WeierstrassCurve there exists a change of variables which will change it into such normal form (WeierstrassCurve.exists_variableChange_isCharThreeNF). See also WeierstrassCurve.toCharThreeNF and WeierstrassCurve.toCharThreeNF_spec.

• WeierstrassCurve.IsCharTwoJEqZeroNF is a type class which asserts that a WeierstrassCurve is of form $Y^2 + a_3Y = X^3 + a_4X + a_6$. It is the normal form of characteristic = 2 and j = 0.

  If the ring is of characteristic = 2, then for any WeierstrassCurve with $a_1 = 0$ (for an elliptic curve, this is equivalent to j = 0), there exists a change of variables which will change it into such normal form (see WeierstrassCurve.toCharTwoJEqZeroNF and WeierstrassCurve.toCharTwoJEqZeroNF_spec).

• WeierstrassCurve.IsCharTwoJNeZeroNF is a type class which asserts that a WeierstrassCurve is of form $Y^2 + XY = X^3 + a_2X^2 + a_6$. It is the normal form of characteristic = 2 and j ≠ 0.

  If the field is of characteristic = 2, then for any WeierstrassCurve with $a_1 \neq 0$ (for an elliptic curve, this is equivalent to j ≠ 0), there exists a change of variables which will change it into such normal form (see WeierstrassCurve.toCharTwoJNeZeroNF and WeierstrassCurve.toCharTwoJNeZeroNF_spec).

• WeierstrassCurve.IsCharTwoNF is the combination of the above two, that is, asserts that a WeierstrassCurve is of form $Y^2 + XY = X^3 + a_2X^2 + a_6$ or $Y^2 + a_3Y = X^3 + a_4X + a_6$. It is the normal form of characteristic = 2.

  If the field is of characteristic = 2, then for any WeierstrassCurve there exists a change of variables which will change it into such normal form (WeierstrassCurve.exists_variableChange_isCharTwoNF). See also WeierstrassCurve.toCharTwoNF and WeierstrassCurve.toCharTwoNF_spec.

References

• J Silverman, The Arithmetic of Elliptic Curves

Tags

elliptic curve, weierstrass equation, normal form

Normal forms of characteristic ≠ 2

class WeierstrassCurve.IsCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in normal form of characteristic ≠ 2, if its $a_1, a_3 = 0$. In other words it is $Y^2 = X^3 + a_2X^2 + a_4X + a_6$.

• a₁ : W.a₁ = 0
• a₃ : W.a₃ = 0

theorem WeierstrassCurve.isCharNeTwoNF_iff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.IsCharNeTwoNF ↔ W.a₁ = 0 ∧ W.a₃ = 0

@[simp]

theorem WeierstrassCurve.a₁_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.a₁ = 0

@[simp]

theorem WeierstrassCurve.a₃_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.a₃ = 0

@[simp]

theorem WeierstrassCurve.b₂_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.b₂ = 4 * W.a₂

@[simp]

theorem WeierstrassCurve.b₄_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.b₄ = 2 * W.a₄

@[simp]

theorem WeierstrassCurve.b₆_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.b₆ = 4 * W.a₆

@[simp]

theorem WeierstrassCurve.b₈_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.b₈ = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

@[simp]

theorem WeierstrassCurve.c₄_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄

@[simp]

theorem WeierstrassCurve.c₆_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.c₆ = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

@[simp]

theorem WeierstrassCurve.Δ_of_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF] : W.Δ = -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

def WeierstrassCurve.toCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : WeierstrassCurve.VariableChange R

There is an explicit change of variables of a WeierstrassCurve to a normal form of characteristic ≠ 2, provided that 2 is invertible in the ring.

Equations

• W.toCharNeTwoNF = { u := 1, r := 0, s := ⅟2 * -W.a₁, t := ⅟2 * -W.a₃ }

@[simp]

theorem WeierstrassCurve.toCharNeTwoNF_u {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : W.toCharNeTwoNF.u = 1

@[simp]

theorem WeierstrassCurve.toCharNeTwoNF_s {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : W.toCharNeTwoNF.s = ⅟2 * -W.a₁

@[simp]

theorem WeierstrassCurve.toCharNeTwoNF_t {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : W.toCharNeTwoNF.t = ⅟2 * -W.a₃

@[simp]

theorem WeierstrassCurve.toCharNeTwoNF_r {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : W.toCharNeTwoNF.r = 0

instance WeierstrassCurve.toCharNeTwoNF_spec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : (W.variableChange W.toCharNeTwoNF).IsCharNeTwoNF

theorem WeierstrassCurve.exists_variableChange_isCharNeTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] : ∃ (C : WeierstrassCurve.VariableChange R), (W.variableChange C).IsCharNeTwoNF

Short normal form

class WeierstrassCurve.IsShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in short normal form, if its $a_1, a_2, a_3 = 0$. In other words it is $Y^2 = X^3 + a_4X + a_6$.

This is the normal form of characteristic ≠ 2 or 3, and also the normal form of characteristic = 3 and j = 0.

• a₁ : W.a₁ = 0
• a₂ : W.a₂ = 0
• a₃ : W.a₃ = 0

theorem WeierstrassCurve.isShortNF_iff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.IsShortNF ↔ W.a₁ = 0 ∧ W.a₂ = 0 ∧ W.a₃ = 0

instance WeierstrassCurve.isCharNeTwoNF_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.IsCharNeTwoNF

theorem WeierstrassCurve.a₁_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.a₁ = 0

@[simp]

theorem WeierstrassCurve.a₂_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.a₂ = 0

theorem WeierstrassCurve.a₃_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.a₃ = 0

theorem WeierstrassCurve.b₂_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.b₂ = 0

theorem WeierstrassCurve.b₄_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.b₄ = 2 * W.a₄

theorem WeierstrassCurve.b₆_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.b₆ = 4 * W.a₆

theorem WeierstrassCurve.b₈_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.b₈ = -W.a₄ ^ 2

theorem WeierstrassCurve.c₄_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.c₄ = -48 * W.a₄

theorem WeierstrassCurve.c₆_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.c₆ = -864 * W.a₆

theorem WeierstrassCurve.Δ_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

theorem WeierstrassCurve.b₄_of_isShortNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3] : W.b₄ = -W.a₄

theorem WeierstrassCurve.b₆_of_isShortNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3] : W.b₆ = W.a₆

theorem WeierstrassCurve.c₄_of_isShortNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3] : W.c₄ = 0

theorem WeierstrassCurve.c₆_of_isShortNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3] : W.c₆ = 0

theorem WeierstrassCurve.Δ_of_isShortNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3] : W.Δ = -W.a₄ ^ 3

theorem WeierstrassCurve.j_of_isShortNF {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsShortNF] : W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

@[simp]

theorem WeierstrassCurve.j_of_isShortNF_of_char_three {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsShortNF] [CharP F 3] : W.j = 0

def WeierstrassCurve.toShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] [Invertible 3] : WeierstrassCurve.VariableChange R

There is an explicit change of variables of a WeierstrassCurve to a short normal form, provided that 2 and 3 are invertible in the ring. It is the composition of an explicit change of variables with WeierstrassCurve.toCharNeTwoNF.

Equations

• W.toShortNF = { u := 1, r := ⅟3 * -(W.variableChange W.toCharNeTwoNF).a₂, s := 0, t := 0 }.comp W.toCharNeTwoNF

instance WeierstrassCurve.toShortNF_spec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] [Invertible 3] : (W.variableChange W.toShortNF).IsShortNF

theorem WeierstrassCurve.exists_variableChange_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [Invertible 2] [Invertible 3] : ∃ (C : WeierstrassCurve.VariableChange R), (W.variableChange C).IsShortNF

Normal forms of characteristic = 3 and j ≠ 0

class WeierstrassCurve.IsCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in normal form of characteristic = 3 and j ≠ 0, if its $a_1, a_3, a_4 = 0$. In other words it is $Y^2 = X^3 + a_2X^2 + a_6$.

• a₁ : W.a₁ = 0
• a₃ : W.a₃ = 0
• a₄ : W.a₄ = 0

theorem WeierstrassCurve.isCharThreeJNeZeroNF_iff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.IsCharThreeJNeZeroNF ↔ W.a₁ = 0 ∧ W.a₃ = 0 ∧ W.a₄ = 0

instance WeierstrassCurve.isCharNeTwoNF_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.IsCharNeTwoNF

theorem WeierstrassCurve.a₁_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.a₁ = 0

theorem WeierstrassCurve.a₃_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.a₃ = 0

@[simp]

theorem WeierstrassCurve.a₄_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.a₄ = 0

theorem WeierstrassCurve.b₂_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.b₂ = 4 * W.a₂

theorem WeierstrassCurve.b₄_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.b₄ = 0

theorem WeierstrassCurve.b₆_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.b₆ = 4 * W.a₆

theorem WeierstrassCurve.b₈_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.b₈ = 4 * W.a₂ * W.a₆

theorem WeierstrassCurve.c₄_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.c₄ = 16 * W.a₂ ^ 2

theorem WeierstrassCurve.c₆_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.c₆ = -64 * W.a₂ ^ 3 - 864 * W.a₆

theorem WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.Δ = -64 * W.a₂ ^ 3 * W.a₆ - 432 * W.a₆ ^ 2

theorem WeierstrassCurve.b₂_of_isCharThreeJNeZeroNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3] : W.b₂ = W.a₂

theorem WeierstrassCurve.b₆_of_isCharThreeJNeZeroNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3] : W.b₆ = W.a₆

theorem WeierstrassCurve.b₈_of_isCharThreeJNeZeroNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3] : W.b₈ = W.a₂ * W.a₆

theorem WeierstrassCurve.c₄_of_isCharThreeJNeZeroNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3] : W.c₄ = W.a₂ ^ 2

theorem WeierstrassCurve.c₆_of_isCharThreeJNeZeroNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3] : W.c₆ = -W.a₂ ^ 3

theorem WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_of_char_three {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3] : W.Δ = -W.a₂ ^ 3 * W.a₆

@[simp]

theorem WeierstrassCurve.j_of_isCharThreeJNeZeroNF_of_char_three {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharThreeJNeZeroNF] [CharP F 3] : W.j = -W.a₂ ^ 3 / W.a₆

theorem WeierstrassCurve.j_ne_zero_of_isCharThreeJNeZeroNF_of_char_three {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharThreeJNeZeroNF] [CharP F 3] : W.j ≠ 0

Normal forms of characteristic = 3

class inductive WeierstrassCurve.IsCharThreeNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in normal form of characteristic = 3, if it is $Y^2 = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharThreeJNeZeroNF) or $Y^2 = X^3 + a_4X + a_6$ (WeierstrassCurve.IsShortNF).

• of_j_ne_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} [W.IsCharThreeJNeZeroNF] : W.IsCharThreeNF
• of_j_eq_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} [W.IsShortNF] : W.IsCharThreeNF

instance WeierstrassCurve.isCharThreeNF_of_isCharThreeJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] : W.IsCharThreeNF

instance WeierstrassCurve.isCharThreeNF_of_isShortNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] : W.IsCharThreeNF

instance WeierstrassCurve.isCharNeTwoNF_of_isCharThreeNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeNF] : W.IsCharNeTwoNF

def WeierstrassCurve.toShortNFOfCharThree {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : WeierstrassCurve.VariableChange R

For a WeierstrassCurve defined over a ring of characteristic = 3, there is an explicit change of variables of it to $Y^2 = X^3 + a_4X + a_6$ (WeierstrassCurve.IsShortNF) if its j = 0. This is in fact given by WeierstrassCurve.toCharNeTwoNF.

Equations

• W.toShortNFOfCharThree = W.toCharNeTwoNF

theorem WeierstrassCurve.toShortNFOfCharThree_a₂ {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] : (W.variableChange W.toShortNFOfCharThree).a₂ = W.b₂

theorem WeierstrassCurve.toShortNFOfCharThree_spec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 3] (hb₂ : W.b₂ = 0) : (W.variableChange W.toShortNFOfCharThree).IsShortNF

def WeierstrassCurve.toCharThreeNF {F : Type u_2} [Field F] [CharP F 3] (W : WeierstrassCurve F) : WeierstrassCurve.VariableChange F

For a WeierstrassCurve defined over a field of characteristic = 3, there is an explicit change of variables of it to WeierstrassCurve.IsCharThreeNF, that is, $Y^2 = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharThreeJNeZeroNF) or $Y^2 = X^3 + a_4X + a_6$ (WeierstrassCurve.IsShortNF). It is the composition of an explicit change of variables with WeierstrassCurve.toShortNFOfCharThree.

Equations

• W.toCharThreeNF = { u := 1, r := (W.variableChange W.toShortNFOfCharThree).a₄ / (W.variableChange W.toShortNFOfCharThree).a₂, s := 0, t := 0 }.comp W.toShortNFOfCharThree

theorem WeierstrassCurve.toCharThreeNF_spec_of_b₂_ne_zero {F : Type u_2} [Field F] [CharP F 3] (W : WeierstrassCurve F) (hb₂ : W.b₂ ≠ 0) : (W.variableChange W.toCharThreeNF).IsCharThreeJNeZeroNF

theorem WeierstrassCurve.toCharThreeNF_spec_of_b₂_eq_zero {F : Type u_2} [Field F] [CharP F 3] (W : WeierstrassCurve F) (hb₂ : W.b₂ = 0) : (W.variableChange W.toCharThreeNF).IsShortNF

instance WeierstrassCurve.toCharThreeNF_spec {F : Type u_2} [Field F] [CharP F 3] (W : WeierstrassCurve F) : (W.variableChange W.toCharThreeNF).IsCharThreeNF

theorem WeierstrassCurve.exists_variableChange_isCharThreeNF {F : Type u_2} [Field F] [CharP F 3] (W : WeierstrassCurve F) : ∃ (C : WeierstrassCurve.VariableChange F), (W.variableChange C).IsCharThreeNF

Normal forms of characteristic = 2 and j ≠ 0

class WeierstrassCurve.IsCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in normal form of characteristic = 2 and j ≠ 0, if its $a_1 = 1$ and $a_3, a_4 = 0$. In other words it is $Y^2 + XY = X^3 + a_2X^2 + a_6$.

• a₁ : W.a₁ = 1
• a₃ : W.a₃ = 0
• a₄ : W.a₄ = 0

theorem WeierstrassCurve.isCharTwoJNeZeroNF_iff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.IsCharTwoJNeZeroNF ↔ W.a₁ = 1 ∧ W.a₃ = 0 ∧ W.a₄ = 0

@[simp]

theorem WeierstrassCurve.a₁_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.a₁ = 1

@[simp]

theorem WeierstrassCurve.a₃_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.a₃ = 0

@[simp]

theorem WeierstrassCurve.a₄_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.a₄ = 0

@[simp]

theorem WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.b₂ = 1 + 4 * W.a₂

@[simp]

theorem WeierstrassCurve.b₄_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.b₄ = 0

@[simp]

theorem WeierstrassCurve.b₆_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.b₆ = 4 * W.a₆

@[simp]

theorem WeierstrassCurve.b₈_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.b₈ = W.a₆ + 4 * W.a₂ * W.a₆

@[simp]

theorem WeierstrassCurve.c₄_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.c₄ = W.b₂ ^ 2

@[simp]

theorem WeierstrassCurve.c₆_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.c₆ = -W.b₂ ^ 3 - 864 * W.a₆

theorem WeierstrassCurve.b₂_of_isCharTwoJNeZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2] : W.b₂ = 1

theorem WeierstrassCurve.b₆_of_isCharTwoJNeZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2] : W.b₆ = 0

theorem WeierstrassCurve.b₈_of_isCharTwoJNeZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2] : W.b₈ = W.a₆

theorem WeierstrassCurve.c₄_of_isCharTwoJNeZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2] : W.c₄ = 1

theorem WeierstrassCurve.c₆_of_isCharTwoJNeZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2] : W.c₆ = 1

@[simp]

theorem WeierstrassCurve.Δ_of_isCharTwoJNeZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] [CharP R 2] : W.Δ = W.a₆

@[simp]

theorem WeierstrassCurve.j_of_isCharTwoJNeZeroNF_of_char_two {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoJNeZeroNF] [CharP F 2] : W.j = 1 / W.a₆

theorem WeierstrassCurve.j_ne_zero_of_isCharTwoJNeZeroNF_of_char_two {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoJNeZeroNF] [CharP F 2] : W.j ≠ 0

Normal forms of characteristic = 2 and j = 0

class WeierstrassCurve.IsCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in normal form of characteristic = 2 and j = 0, if its $a_1, a_2 = 0$. In other words it is $Y^2 + a_3Y = X^3 + a_4X + a_6$.

• a₁ : W.a₁ = 0
• a₂ : W.a₂ = 0

theorem WeierstrassCurve.isCharTwoJEqZeroNF_iff {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : W.IsCharTwoJEqZeroNF ↔ W.a₁ = 0 ∧ W.a₂ = 0

@[simp]

theorem WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.a₁ = 0

@[simp]

theorem WeierstrassCurve.a₂_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.a₂ = 0

@[simp]

theorem WeierstrassCurve.b₂_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.b₂ = 0

@[simp]

theorem WeierstrassCurve.b₄_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.b₄ = 2 * W.a₄

@[simp]

theorem WeierstrassCurve.b₈_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.b₈ = -W.a₄ ^ 2

@[simp]

theorem WeierstrassCurve.c₄_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.c₄ = -48 * W.a₄

@[simp]

theorem WeierstrassCurve.c₆_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.c₆ = -216 * W.b₆

@[simp]

theorem WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.Δ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

theorem WeierstrassCurve.b₄_of_isCharTwoJEqZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2] : W.b₄ = 0

theorem WeierstrassCurve.b₈_of_isCharTwoJEqZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2] : W.b₈ = W.a₄ ^ 2

theorem WeierstrassCurve.c₄_of_isCharTwoJEqZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2] : W.c₄ = 0

theorem WeierstrassCurve.c₆_of_isCharTwoJEqZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2] : W.c₆ = 0

theorem WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF_of_char_two {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2] : W.Δ = W.a₃ ^ 4

theorem WeierstrassCurve.j_of_isCharTwoJEqZeroNF {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoJEqZeroNF] : W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)

@[simp]

theorem WeierstrassCurve.j_of_isCharTwoJEqZeroNF_of_char_two {F : Type u_2} [Field F] (W : WeierstrassCurve F) [W.IsElliptic] [W.IsCharTwoJEqZeroNF] [CharP F 2] : W.j = 0

Normal forms of characteristic = 2

class inductive WeierstrassCurve.IsCharTwoNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : Prop

A WeierstrassCurve is in normal form of characteristic = 2, if it is $Y^2 + XY = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharTwoJNeZeroNF) or $Y^2 + a_3Y = X^3 + a_4X + a_6$ (WeierstrassCurve.IsCharTwoJEqZeroNF).

• of_j_ne_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} [W.IsCharTwoJNeZeroNF] : W.IsCharTwoNF
• of_j_eq_zero {R : Type u_1} [CommRing R] {W : WeierstrassCurve R} [W.IsCharTwoJEqZeroNF] : W.IsCharTwoNF

instance WeierstrassCurve.isCharTwoNF_of_isCharTwoJNeZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF] : W.IsCharTwoNF

instance WeierstrassCurve.isCharTwoNF_of_isCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] : W.IsCharTwoNF

def WeierstrassCurve.toCharTwoJEqZeroNF {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) : WeierstrassCurve.VariableChange R

For a WeierstrassCurve defined over a ring of characteristic = 2, there is an explicit change of variables of it to $Y^2 + a_3Y = X^3 + a_4X + a_6$ (WeierstrassCurve.IsCharTwoJEqZeroNF) if its j = 0.

Equations

• W.toCharTwoJEqZeroNF = { u := 1, r := W.a₂, s := 0, t := 0 }

theorem WeierstrassCurve.toCharTwoJEqZeroNF_spec {R : Type u_1} [CommRing R] (W : WeierstrassCurve R) [CharP R 2] (ha₁ : W.a₁ = 0) : (W.variableChange W.toCharTwoJEqZeroNF).IsCharTwoJEqZeroNF

def WeierstrassCurve.toCharTwoJNeZeroNF {F : Type u_2} [Field F] (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0) : WeierstrassCurve.VariableChange F

For a WeierstrassCurve defined over a field of characteristic = 2, there is an explicit change of variables of it to $Y^2 + XY = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharTwoJNeZeroNF) if its j ≠ 0.

Equations

• W.toCharTwoJNeZeroNF ha₁ = { u := Units.mk0 W.a₁ ha₁, r := W.a₃ / W.a₁, s := 0, t := (W.a₁ ^ 2 * W.a₄ + W.a₃ ^ 2) / W.a₁ ^ 3 }

theorem WeierstrassCurve.toCharTwoJNeZeroNF_spec {F : Type u_2} [Field F] [CharP F 2] (W : WeierstrassCurve F) (ha₁ : W.a₁ ≠ 0) : (W.variableChange (W.toCharTwoJNeZeroNF ha₁)).IsCharTwoJNeZeroNF

def WeierstrassCurve.toCharTwoNF {F : Type u_2} [Field F] (W : WeierstrassCurve F) [DecidableEq F] : WeierstrassCurve.VariableChange F

For a WeierstrassCurve defined over a field of characteristic = 2, there is an explicit change of variables of it to WeierstrassCurve.IsCharTwoNF, that is, $Y^2 + XY = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharTwoJNeZeroNF) or $Y^2 + a_3Y = X^3 + a_4X + a_6$ (WeierstrassCurve.IsCharTwoJEqZeroNF).

Equations

• W.toCharTwoNF = if ha₁ : W.a₁ = 0 then W.toCharTwoJEqZeroNF else W.toCharTwoJNeZeroNF ha₁

instance WeierstrassCurve.toCharTwoNF_spec {F : Type u_2} [Field F] [CharP F 2] (W : WeierstrassCurve F) [DecidableEq F] : (W.variableChange W.toCharTwoNF).IsCharTwoNF

theorem WeierstrassCurve.exists_variableChange_isCharTwoNF {F : Type u_2} [Field F] [CharP F 2] (W : WeierstrassCurve F) : ∃ (C : WeierstrassCurve.VariableChange F), (W.variableChange C).IsCharTwoNF