Documentation

TauCeti.AlgebraicGeometry.EllipticCurve.CurveX3SubX

The curve y² = x³ - x #

The Weierstrass curve y² = x³ - x has discriminant 64, so it is an elliptic curve over every field of characteristic other than two. Its points of order dividing two are the point at infinity O and the three points T₀ = (0, 0), T₁ = (1, 0) and T₋₁ = (-1, 0) on the line y = 0, all rational over the base field.

Main definitions #

Main results #

source
def TauCeti.CurveX3SubX.curve (R : Type u_1) [CommRing R] :
WeierstrassCurve R

The Weierstrass curve y² = x³ - x.

Instances For
    source
    @[simp]
    theorem TauCeti.CurveX3SubX.curve_a₁ (R : Type u_1) [CommRing R] :
    (curve R).a₁ = 0

    The coefficient a₁ of y² = x³ - x is 0.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.curve_a₂ (R : Type u_1) [CommRing R] :
    (curve R).a₂ = 0

    The coefficient a₂ of y² = x³ - x is 0.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.curve_a₃ (R : Type u_1) [CommRing R] :
    (curve R).a₃ = 0

    The coefficient a₃ of y² = x³ - x is 0.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.curve_a₄ (R : Type u_1) [CommRing R] :
    (curve R).a₄ = -1

    The coefficient a₄ of y² = x³ - x is -1.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.curve_a₆ (R : Type u_1) [CommRing R] :
    (curve R).a₆ = 0

    The coefficient a₆ of y² = x³ - x is 0.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.Δ_curve (R : Type u_1) [CommRing R] :
    (curve R).Δ = 64

    The discriminant of y² = x³ - x is 64.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.map_curve {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) :
    (curve R).map f = curve S

    y² = x³ - x is defined over ℤ, so it is preserved by every ring homomorphism.

    source
    @[simp]
    theorem TauCeti.CurveX3SubX.equation_iff {R : Type u_1} [CommRing R] (x y : R) :
    (curve R).toAffine.Equation x y ↔ y ^ 2 = x ^ 3 - x

    The affine points of y² = x³ - x are the solutions of y² = x³ - x.

    source
    instance TauCeti.CurveX3SubX.instIsEllipticCurveOfNeZeroOfNat (K : Type u_1) [Field K] [NeZero 2] :
    (curve K).IsElliptic

    Away from characteristic two, y² = x³ - x is an elliptic curve: its discriminant 64 = 2⁶ is a unit.

    source
    def TauCeti.CurveX3SubX.pointZero (K : Type u_1) [Field K] :
    (curve K).toAffine.Point

    The point T₀ = (0, 0) of y² = x³ - x. It is a nonsingular point in every characteristic, including two.

    Instances For
      source
      @[simp]
      theorem TauCeti.CurveX3SubX.pointZero_ne_zero {K : Type u_1} [Field K] :
      pointZero K ≠ 0

      T₀ is not the point at infinity.

      source
      def TauCeti.CurveX3SubX.pointOne (K : Type u_1) [Field K] [NeZero 2] :
      (curve K).toAffine.Point

      The point T₁ = (1, 0) of y² = x³ - x.

      Instances For
        source
        def TauCeti.CurveX3SubX.pointNegOne (K : Type u_1) [Field K] [NeZero 2] :
        (curve K).toAffine.Point

        The point T₋₁ = (-1, 0) of y² = x³ - x.

        Instances For
          source
          @[simp]
          theorem TauCeti.CurveX3SubX.pointOne_ne_zero {K : Type u_1} [Field K] [NeZero 2] :
          pointOne K ≠ 0

          T₁ is not the point at infinity.

          source
          @[simp]
          theorem TauCeti.CurveX3SubX.pointNegOne_ne_zero {K : Type u_1} [Field K] [NeZero 2] :
          pointNegOne K ≠ 0

          T₋₁ is not the point at infinity.

          source
          @[simp]
          theorem TauCeti.CurveX3SubX.pointZero_ne_pointOne {K : Type u_1} [Field K] [NeZero 2] :
          pointZero K ≠ pointOne K

          T₀ ≠ T₁.

          source
          @[simp]
          theorem TauCeti.CurveX3SubX.pointZero_ne_pointNegOne {K : Type u_1} [Field K] [NeZero 2] :
          pointZero K ≠ pointNegOne K

          T₀ ≠ T₋₁.

          source
          @[simp]
          theorem TauCeti.CurveX3SubX.pointOne_ne_pointNegOne {K : Type u_1} [Field K] [NeZero 2] :
          pointOne K ≠ pointNegOne K

          T₁ ≠ T₋₁, since 1 ≠ -1 away from characteristic two.

          source
          @[simp]
          theorem TauCeti.CurveX3SubX.neg_eq_self_iff {K : Type u_1} [Field K] [NeZero 2] (T : (curve K).toAffine.Point) :
          -T = T ↔ T = 0 ∨ T = pointZero K ∨ T = pointOne K ∨ T = pointNegOne K

          The points of order dividing two on y² = x³ - x are the point at infinity and the three points (0, 0), (1, 0) and (-1, 0) on the line y = 0.