Step 29 / 64

University

The quantity c₄, from coefficients to a fingerprint

A short polynomial in the coefficients that tells how badly the curve breaks.

Start with a concrete example

For the equation y²=x³−x, a fixed recipe gives c₄=48. Think of it as a number calculated from the equation, like an area calculated from side lengths, not an extra point on the drawing.

A small check: try the idea

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

In the example y²=x³−x, what is c₄=48 describing?

Read the answer and reasoning

A number calculated from the equation. The fixed recipe produces a numerical invariant. It is not a pair (x,y) naming a point on the curve.

Build the idea in three steps

  1. Five coefficients are a lot to carry. The library first condenses them into four helper quantities — b₂, b₄, b₆ and b₈ — each a short polynomial in the coefficients.
  2. The c-quantities combine the helpers further. The one our proof leans on is c₄ = b₂² − 24·b₄: a single summary number computed straight from the curve’s coefficients.
  3. The two summary numbers divide the work: Δ records where the curve breaks, and c₄ tells how badly. Semistability demands that every prime dividing Δ spare c₄ — the tame kind of breakdown.

A small example

Take y² = x³ − x, i.e. a₄ = −1 with the other coefficients 0. Then b₂ = 0 and b₄ = 2·(−1) = −2, so c₄ = 0² − 24·(−2) = 48 — a nonzero fingerprint.

Lean definition · original excerpt

Mathlib · db584cd · Weierstrass.lean

/-- The `b₂` coefficient of a Weierstrass curve. -/def b₂ : R :=  W.a₁ ^ 2 + 4 * W.a₂ /-- The `b₄` coefficient of a Weierstrass curve. -/def b₄ : R :=  2 * W.a₄ + W.a₁ * W.a₃ /-- The `b₆` coefficient of a Weierstrass curve. -/def b₆ : R :=  W.a₃ ^ 2 + 4 * W.a₆ /-- The `b₈` coefficient of a Weierstrass curve. -/def b₈ : R :=  W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 lemma b_relation : 4 * W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2 := by  simp only [b₂, b₄, b₆, b₈]  ring1 /-- The `c₄` coefficient of a Weierstrass curve. -/def c₄ : R :=  W.b₂ ^ 2 - 24 * W.b₄

How to read this Lean

Every displayed definition is one short composition: b₄, for instance, mixes 2·a₄ with a₁·a₃. The lemma b_relation in the middle ties b₈ to b₂, b₆ and b₄ — Lean keeps the bookkeeping identities beside the definitions. Farther down the same file, the identity 1728·Δ = c₄³ − c₆² connects this block to the discriminant page.

Where this idea is used

9. 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

The quantity c₄, from coefficients to a fingerprint

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 short polynomial in the coefficients that tells how badly the curve breaks.

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

A small clue

Take y² = x³ − x, i.e. a₄ = −1 with the other coefficients 0. Then b₂ = 0 and b₄ = 2·(−1) = −2, so c₄ = 0² − 24·(−2) = 48 — a nonzero fingerprint.

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 →