funlean.
順番 29 / 64

大学

量c₄——係数から指紋へ

係数の短い多項式から、曲線の壊れ方の激しさを伝える数を作ります。

まず、身近な例で

y²=x³−xという式から、決まった計算でc₄=48が出ます。辺の長さから面積を計算するように、式から作る数です。絵の上に新しい点がある、という意味ではありません。

ちいさな確認：考えてみよう

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

例のy²=x³−xで、c₄=48とは何？

答えと考え方を読む

方程式から計算する数。 決まった計算で得られる数です。曲線上の点を表す(x,y)の組ではありません。

3段階で考えよう

  1. 係数は五つもあり、持ち歩くには重い。ライブラリはまず、係数の短い多項式である四つの助けの量——b₂・b₄・b₆・b₈——に凝縮します。
  2. cの量は、その助けをさらに合成します。証明が頼るのはc₄ = b₂² − 24·b₄。曲線の係数から直接計算される、一つのまとめの数です。
  3. 二つのまとめの数は役割を分けます:Δは曲線がどこで壊れるかを記録し、c₄は壊れ方の激しさを伝えます。半安定性は、「Δを割るすべての素数がc₄を割らない」ことを要求します。おとなしい種類の壊れ方です。

小さな例で確かめる

y² = x³ − x、つまりa₄ = −1で他の係数は0としてみます。b₂ = 0、b₄ = 2·(−1) = −2なので、c₄ = 0² − 24·(−2) = 48。ゼロでない指紋です。

Leanの定義・原文の抜粋

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₄

このLeanの読み方

どの定義も短い合成です。たとえばb₄は2·a₄とa₁·a₃を混ぜます。途中に見える補題b_relationは、b₈をb₂・b₆・b₄で結びます。Leanは、こうした帳簿の等式を定義のそばに置いておきます。同じファイルのさらに下では、恒等式1728·Δ = c₄³ − c₆²がこのブロックを判別式のページへつなぎます。

元の原文 ↗ · L100–122保存した原文全体を開く

この言葉を使う章

9. コンサートへの二つの入口10. 3音だけのオーディション11. パスポートを借りる作戦12. 二つの工房、同じ注文13. ピップの無謀なキルト14. どんどん小さくなる予約16. 入れないはずの客
わからない・道に迷った

ミカのたすけ舟

量c₄——係数から指紋へ

今は、一つだけ

まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。

言葉をほどこう

係数の短い多項式から、曲線の壊れ方の激しさを伝える数を作ります。

このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。

小さな手がかり

y² = x³ − x、つまりa₄ = −1で他の係数は0としてみます。b₂ = 0、b₄ = 2·(−1) = −2なので、c₄ = 0² − 24·(−2) = 48。ゼロでない指紋です。

閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。

最初の小さな物語から読む →