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_1, a_3 = 0$. In other words it is $Y^2 = X^3 + a_2X^2 + a_4X + a_6$.

Instances

    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
    Instances For

      Short normal form #

      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.

      Instances

        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
        Instances For

          Normal forms of characteristic = 3 and j ≠ 0 #

          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$.

          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^2 = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharThreeJNeZeroNF) or $Y^2 = X^3 + a_4X + a_6$ (WeierstrassCurve.IsShortNF).

            Instances

              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
              Instances For

                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
                Instances For

                  Normal forms of characteristic = 2 and j ≠ 0 #

                  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$.

                  Instances

                    Normal forms of characteristic = 2 and j = 0 #

                    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$.

                    Instances

                      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^2 + XY = X^3 + a_2X^2 + a_6$ (WeierstrassCurve.IsCharTwoJNeZeroNF) or $Y^2 + a_3Y = X^3 + a_4X + a_6$ (WeierstrassCurve.IsCharTwoJEqZeroNF).

                      Instances

                        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
                        Instances For

                          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
                          Instances For

                            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
                            Instances For