funlean.
Step 27 / 64

High school

Curves defined by equations

An equation describes pairs of coordinates satisfying it.

Start with a concrete example

The equation y=x² selects points such as (−2,4),(0,0),(2,4). Drawing the selected points gives a curve. The curves in FLT use a different equation, involving y² and x³.

A small check: try the idea

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

Is (2,4) on the curve y=x²?

Read the answer and reasoning

Yes. Substitute x=2: x²=4, matching y. The equation, not equality of the two coordinates, decides membership.

Build the idea in three steps

  1. An equation in x and y specifies coordinate pairs satisfying it. Its points are more important than the shape of a drawing.
  2. A Weierstrass equation has the displayed form with five coefficients. Lean stores those coefficients in a structure.
  3. A nonsingular Weierstrass curve with its distinguished point gives an elliptic curve. The extra condition matters; not every coefficient choice is nonsingular.

A small example

The general equation is y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆. A Frey package supplies a particular choice of coefficients.

Lean definition · original excerpt

Mathlib · db584cd · Weierstrass.lean

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

R is the type of coefficients. The five fields store a₁, a₂, a₃, a₄ and a₆; this structure alone does not certify nonsingularity.

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

Where this idea is used

5. The suspicious parcel6. The scissors incident8. The secret duet9. Two doors to the concert10. A three-note audition11. Borrow a better passport12. The workshops agree13. Pip’s impossible quilt14. The shrinking reservation16. The room with no room
I’m lost · Help

Mika’s help desk

Curves defined by equations

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

An equation describes pairs of coordinates satisfying it.

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

A small clue

The general equation is y² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆. A Frey package supplies a particular choice of coefficients.

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 →