funlean.
Step 32 / 64

University

The Weierstrass standard form

Five coefficients fix one standard shape for the curves used here.

Start with a concrete example

In y²=x³−x, the numbers multiplying x² and the constant term are both 0. We can write x³+0x²−1x+0 to see the coefficient slots. The general Weierstrass form has five slots.

A small check: try the idea

Think with the concrete example above. You can try again.

In x³+0x²−1x+0, what is the coefficient of x?

Read the answer and reasoning

−1. The x term is −1×x. The zeros belong to the x² and constant slots in this example.

Build the idea in three steps

  1. A long polynomial equation in x and y can hide several component shapes at once. This proof therefore treats one shaped family that is still general enough.
  2. With a suitable change of coordinates, an appropriate cubic equation can be written as y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆. This is the Weierstrass form.
  3. The five coefficients are stored in separate named fields of one structure: a₁, a₂, a₃, a₄ and a₆, each drawn from a coefficient type R.

A small example

The equation y² = x³ − x fits the form: reading the right side as x³ + 0x² + (−1)x + 0 gives a₁ = a₂ = a₃ = 0, a₄ = −1 and a₆ = 0.

Lean definition · original excerpt

Mathlib · db584cd · Weierstrass.lean

/-- A Weierstrass curve `Y² + a₁XY + a₃Y = X³ + a₂X² + a₄X + a₆` with parameters `aᵢ`. -/@[ext]structure WeierstrassCurve (R : Type u) where  /-- The `a₁` coefficient of a Weierstrass curve. -/  a₁ : R  /-- The `a₂` coefficient of a Weierstrass curve. -/  a₂ : R  /-- The `a₃` coefficient of a Weierstrass curve. -/  a₃ : R  /-- The `a₄` coefficient of a Weierstrass curve. -/  a₄ : R  /-- The `a₆` coefficient of a Weierstrass curve. -/  a₆ : R

How to read this Lean

The docstring above the structure states the equation. Each named field stores one coefficient, and the type R declares which kind of numbers the coefficients may come from. This structure holds data only.

Original source ↗ · L75–87Open the complete saved source

Where this idea is used

5. The suspicious parcel
I’m lost · Help

Mika’s help desk

The Weierstrass standard form

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Five coefficients fix one standard shape for the curves used here.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

The equation y² = x³ − x fits the form: reading the right side as x³ + 0x² + (−1)x + 0 gives a₁ = a₂ = a₃ = 0, a₄ = −1 and a₆ = 0.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →