Documentation

Mathlib.AlgebraicGeometry.EllipticCurve.Group

Group law on Weierstrass curves #

This file proves that the nonsingular rational points on a Weierstrass curve forms an abelian group under the geometric group law defined in Mathlib.AlgebraicGeometry.EllipticCurve.Affine and in Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.

Mathematical background #

Let W be a Weierstrass curve over a field F given by a Weierstrass equation $W(X, Y) = 0$ in affine coordinates. As in Mathlib.AlgebraicGeometry.EllipticCurve.Affine, the set of nonsingular rational points W⟮F⟯ of W consist of the unique point at infinity $0$ and nonsingular affine points $(x, y)$. With this description, there is an addition-preserving injection between W⟮F⟯ and the ideal class group of the coordinate ring $F[W] := F[X, Y] / \langle W(X, Y)\rangle$ of W. This is defined by mapping the point at infinity $0$ to the trivial ideal class and an affine point $(x, y)$ to the ideal class of the invertible fractional ideal $\langle X - x, Y - y\rangle$. Proving that this is well-defined and preserves addition reduce to checking several equalities of integral ideals, which is done in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul and in WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal via explicit ideal computations. Now $F[W]$ is a free rank two $F[X]$-algebra with basis $\{1, Y\}$, so every element of $F[W]$ is of the form $p + qY$ for some $p, q \in F[X]$, and there is an algebra norm $N : F[W] \to F[X]$. Injectivity can then be shown by computing the degree of such a norm $N(p + qY)$ in two different ways, which is done in WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis and in the auxiliary lemmas in the proof of WeierstrassCurve.Affine.Point.instAddCommGroup.

When W is given in Jacobian coordinates, WeierstrassCurve.Jacobian.Point.toAffineAddEquiv pulls back the group law on WeierstrassCurve.Affine.Point to WeierstrassCurve.Jacobian.Point.

Main definitions #

Main statements #

References #

https://drops.dagstuhl.de/storage/00lipics/lipics-vol268-itp2023/LIPIcs.ITP.2023.6/LIPIcs.ITP.2023.6.pdf

Tags #

elliptic curve, group law, class group

Weierstrass curves in affine coordinates #

@[reducible, inline]

The coordinate ring $R[W] := R[X, Y] / \langle W(X, Y) \rangle$ of W.

Equations
Instances For
    @[reducible, inline]

    The function field $R(W) := \mathrm{Frac}(R[W])$ of W.

    Equations
    Instances For

      The coordinate ring as an R[X]-algebra #

      @[reducible, inline]
      noncomputable abbrev WeierstrassCurve.Affine.CoordinateRing.mk {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
      Polynomial (Polynomial R) →+* W.CoordinateRing

      The natural ring homomorphism mapping an element of R[X][Y] to an element of R[W].

      Equations
      Instances For
        noncomputable def WeierstrassCurve.Affine.CoordinateRing.basis {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) :
        Basis (Fin 2) (Polynomial R) W.CoordinateRing

        The basis $\{1, Y\}$ for the coordinate ring $R[W]$ over the polynomial ring $R[X]$.

        Equations
        Instances For
          theorem WeierstrassCurve.Affine.CoordinateRing.smul {R : Type u} [CommRing R] {W : WeierstrassCurve.Affine R} (x : Polynomial R) (y : W.CoordinateRing) :
          theorem WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (p : Polynomial R) (q : Polynomial R) :
          (p 1 + q (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X) * (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X = (q * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)) 1 + (p - q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)) (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X
          noncomputable def WeierstrassCurve.Affine.CoordinateRing.map {R : Type u} {S : Type v} [CommRing R] [CommRing S] (W : WeierstrassCurve.Affine R) (f : R →+* S) :
          W.CoordinateRing →+* (WeierstrassCurve.map W f).toAffine.CoordinateRing

          The ring homomorphism R[W] →+* S[W.map f] induced by a ring homomorphism f : R →+* S.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            • =

            Ideals in the coordinate ring over a ring #

            noncomputable def WeierstrassCurve.Affine.CoordinateRing.XClass {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) :
            W.CoordinateRing

            The class of the element $X - x$ in $R[W]$ for some $x \in R$.

            Equations
            Instances For
              noncomputable def WeierstrassCurve.Affine.CoordinateRing.YClass {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (y : Polynomial R) :
              W.CoordinateRing

              The class of the element $Y - y(X)$ in $R[W]$ for some $y(X) \in R[X]$.

              Equations
              Instances For
                theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : R) (L : R) :
                (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.addPolynomial x y L)) = (WeierstrassCurve.Affine.CoordinateRing.mk W) ((Polynomial.X - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)) * (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)))
                noncomputable def WeierstrassCurve.Affine.CoordinateRing.XIdeal {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) :
                Ideal W.CoordinateRing

                The ideal $\langle X - x \rangle$ of $R[W]$ for some $x \in R$.

                Equations
                Instances For
                  noncomputable def WeierstrassCurve.Affine.CoordinateRing.YIdeal {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (y : Polynomial R) :
                  Ideal W.CoordinateRing

                  The ideal $\langle Y - y(X) \rangle$ of $R[W]$ for some $y(X) \in R[X]$.

                  Equations
                  Instances For
                    noncomputable def WeierstrassCurve.Affine.CoordinateRing.XYIdeal {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x : R) (y : Polynomial R) :
                    Ideal W.CoordinateRing

                    The ideal $\langle X - x, Y - y(X) \rangle$ of $R[W]$ for some $x \in R$ and $y(X) \in R[X]$.

                    Equations
                    Instances For
                      theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (x₁ : R) (x₂ : R) (y₁ : R) (L : R) :
                      WeierstrassCurve.Affine.CoordinateRing.XYIdeal W (W.addX x₁ x₂ L) (Polynomial.C (W.addY x₁ x₂ y₁ L)) = Ideal.span {(WeierstrassCurve.Affine.CoordinateRing.mk W) (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x₁ y₁ L))} WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ L)

                      The $R$-algebra isomorphism from $R[W] / \langle X - x, Y - y(X) \rangle$ to $R$ obtained by evaluation at $y(X)$ and at $x$ provided that $W(x, y(x)) = 0$.

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

                        Ideals in the coordinate ring over a field #

                        theorem WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                        (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(WeierstrassCurve.Affine.CoordinateRing.XClass W x₁ * WeierstrassCurve.Affine.CoordinateRing.XClass W x₂ * WeierstrassCurve.Affine.CoordinateRing.XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
                        theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_eq₂ {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                        theorem WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :
                        WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁) * WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂)) = WeierstrassCurve.Affine.CoordinateRing.YIdeal W (WeierstrassCurve.Affine.linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * WeierstrassCurve.Affine.CoordinateRing.XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (Polynomial.C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))
                        noncomputable def WeierstrassCurve.Affine.CoordinateRing.XYIdeal' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x : F} {y : F} (h : W.Nonsingular x y) :
                        (FractionalIdeal (nonZeroDivisors W.CoordinateRing) W.FunctionField)ˣ

                        The non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ for some $x, y \in F$.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal' {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x₁ : F} {x₂ : F} {y₁ : F} {y₂ : F} (h₁ : W.Nonsingular x₁ y₁) (h₂ : W.Nonsingular x₂ y₂) (hxy : x₁ = x₂y₁ W.negY x₂ y₂) :

                          Norms on the coordinate ring #

                          theorem WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (p : Polynomial R) (q : Polynomial R) :
                          (Algebra.norm (Polynomial R)) (p 1 + q (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X) = p ^ 2 - p * q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) - q ^ 2 * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)
                          theorem WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis {R : Type u} [CommRing R] (W : WeierstrassCurve.Affine R) (p : Polynomial R) (q : Polynomial R) :
                          (AdjoinRoot.of W.polynomial) ((Algebra.norm (Polynomial R)) (p 1 + q (WeierstrassCurve.Affine.CoordinateRing.mk W) Polynomial.X)) = (WeierstrassCurve.Affine.CoordinateRing.mk W) ((Polynomial.C p + Polynomial.C q * Polynomial.X) * (Polynomial.C p + Polynomial.C q * (-Polynomial.X - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃))))

                          The axioms for nonsingular rational points on a Weierstrass curve #

                          noncomputable def WeierstrassCurve.Affine.Point.toClassFun {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                          W.PointAdditive (ClassGroup W.CoordinateRing)

                          The set function mapping an affine point $(x, y)$ of W to the class of the non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$.

                          Equations
                          Instances For
                            @[simp]
                            theorem WeierstrassCurve.Affine.Point.toClass_apply {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                            ∀ (a : W.Point), WeierstrassCurve.Affine.Point.toClass a = a.toClassFun
                            noncomputable def WeierstrassCurve.Affine.Point.toClass {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                            W.Point →+ Additive (ClassGroup W.CoordinateRing)

                            The group homomorphism mapping an affine point $(x, y)$ of W to the class of the non-zero fractional ideal $\langle X - x, Y - y \rangle$ of $F(W)$ in the class group of $F[W]$.

                            Equations
                            • WeierstrassCurve.Affine.Point.toClass = { toFun := WeierstrassCurve.Affine.Point.toClassFun, map_zero' := , map_add' := }
                            Instances For
                              theorem WeierstrassCurve.Affine.Point.toClass_zero {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                              WeierstrassCurve.Affine.Point.toClass 0 = 0
                              theorem WeierstrassCurve.Affine.Point.toClass_some {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} {x : F} {y : F} (h : W.Nonsingular x y) :
                              WeierstrassCurve.Affine.Point.toClass (WeierstrassCurve.Affine.Point.some h) = ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h)
                              theorem WeierstrassCurve.Affine.Point.toClass_eq_zero {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} (P : W.Point) :
                              WeierstrassCurve.Affine.Point.toClass P = 0 P = 0
                              theorem WeierstrassCurve.Affine.Point.toClass_injective {F : Type u} [Field F] {W : WeierstrassCurve.Affine F} :
                              Function.Injective WeierstrassCurve.Affine.Point.toClass
                              Equations

                              Weierstrass curves in Jacobian coordinates #

                              Equations

                              Elliptic curves in affine coordinates #

                              def EllipticCurve.Affine.Point.mk {R : Type} [Nontrivial R] [CommRing R] (E : EllipticCurve R) {x : R} {y : R} (h : E.toAffine.Equation x y) :
                              E.toAffine.Point

                              An affine point on an elliptic curve E over R.

                              Equations
                              Instances For