funlean.
Step 33 / 64

University

From the equation to a curve

A forbidden solution supplies explicit coefficients of a Weierstrass curve.

Start with a concrete example

A parcel may need both its contents and a checklist proving it is safe to send. A Frey package similarly bundles numbers with evidence of the required equations and conditions. A list of numbers alone is not enough.

A small check: try the idea

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

Is a list of numbers enough to complete the Frey package?

Read the answer and reasoning

No; evidence of its conditions is also required. The parcel needs both contents and the required checked conditions. In Lean these evidence fields are part of the package.

Build the idea in three steps

  1. The forbidden equation a ^ p + b ^ p = c ^ p is not yet geometry. The next move turns it into coefficients.
  2. FreyPackage.freyCurve takes the package’s integers a, b and exponent p and fixes the five coefficients of a Weierstrass curve over ℚ, for example a₄ = −(a ^ p) · (b ^ p) / 16.
  3. From here the story concerns that curve: its reduction at each prime, its arithmetic data, and eventually its modularity. The integer equation stays encoded in the curve.

A small example

The coefficients are explicit formulas: for chosen integers a and b and exponent p, the displayed a₄ = −(a ^ p) · (b ^ p) / 16 is a definite rational number.

Lean definition · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_FreyPackage.lean

def freyCurve (P : FreyPackage) : WeierstrassCurve ℚ where  a₁ := 1  a₂ := (P.b ^ P.p - 1 - P.a ^ P.p) / 4  a₃ := 0  a₄ := -(P.a ^ P.p) * (P.b ^ P.p) / 16  a₆ := 0

How to read this Lean

Each field is an explicit rational expression in a, b and p; the divisions by 4 and 16 belong to the construction. Its sibling freyCurveInt is the integer-coefficient version used in definitions about reduction.

Original source ↗ · L90–95Open the complete saved source

Where this idea is used

5. The suspicious parcel11. Borrow a better passport
I’m lost · Help

Mika’s help desk

From the equation to a curve

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

A forbidden solution supplies explicit coefficients of a Weierstrass curve.

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

A small clue

The coefficients are explicit formulas: for chosen integers a and b and exponent p, the displayed a₄ = −(a ^ p) · (b ^ p) / 16 is a definite rational number.

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 →