Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

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 [silverman2009], section III.1, page 42.

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

References #

Tags #

elliptic curve, weierstrass equation, normal form

Normal forms of characteristic ≠ 2 #

A WeierstrassCurve is in normal form of characteristic ≠ 2, if its a₁, a₃ = 0. In other words it is Y² = X³ + a₂X² + a₄X + a₆.

Instances
    @[simp]
    @[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₆

    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

    Short normal form #

    A WeierstrassCurve is in short normal form, if its a₁, a₂, a₃ = 0. In other words it is Y² = X³ + a₄X + a₆.

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

    Instances
      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.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)

      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

      Normal forms of characteristic = 3 and j ≠ 0 #

      A WeierstrassCurve is in normal form of characteristic = 3 and j ≠ 0, if its a₁, a₃, a₄ = 0. In other words it is Y² = X³ + a₂X² + a₆.

      Instances

        Normal forms of characteristic = 3 #

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

        A WeierstrassCurve is in normal form of characteristic = 3, if it is Y² = X³ + a₂X² + a₆ (WeierstrassCurve.IsCharThreeJNeZeroNF) or Y² = X³ + a₄X + a₆ (WeierstrassCurve.IsShortNF).

        Instances

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

          Equations

          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² = X³ + a₂X² + a₆ (WeierstrassCurve.IsCharThreeJNeZeroNF) or Y² = X³ + a₄X + a₆ (WeierstrassCurve.IsShortNF). It is the composition of an explicit change of variables with WeierstrassCurve.toShortNFOfCharThree.

          Equations

          Normal forms of characteristic = 2 and j ≠ 0 #

          A WeierstrassCurve is in normal form of characteristic = 2 and j ≠ 0, if its a₁ = 1 and a₃, a₄ = 0. In other words it is Y² + XY = X³ + a₂X² + a₆.

          Instances

            Normal forms of characteristic = 2 and j = 0 #

            A WeierstrassCurve is in normal form of characteristic = 2 and j = 0, if its a₁, a₂ = 0. In other words it is Y² + a₃Y = X³ + a₄X + a₆.

            Instances
              @[simp]
              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)

              Normal forms of characteristic = 2 #

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

              A WeierstrassCurve is in normal form of characteristic = 2, if it is Y² + XY = X³ + a₂X² + a₆ (WeierstrassCurve.IsCharTwoJNeZeroNF) or Y² + a₃Y = X³ + a₄X + a₆ (WeierstrassCurve.IsCharTwoJEqZeroNF).

              Instances

                For a WeierstrassCurve defined over a ring of characteristic = 2, there is an explicit change of variables of it to Y² + a₃Y = X³ + a₄X + a₆ (WeierstrassCurve.IsCharTwoJEqZeroNF) if its j = 0.

                Equations

                For a WeierstrassCurve defined over a field of characteristic = 2, there is an explicit change of variables of it to Y² + XY = X³ + a₂X² + a₆ (WeierstrassCurve.IsCharTwoJNeZeroNF) if its j ≠ 0.

                Equations

                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² + XY = X³ + a₂X² + a₆ (WeierstrassCurve.IsCharTwoJNeZeroNF) or Y² + a₃Y = X³ + a₄X + a₆ (WeierstrassCurve.IsCharTwoJEqZeroNF).

                Equations