3段階で考えよう
- xとyの方程式で、それを満たす座標の組を決めます。絵の形より、どの点が条件を満たすかが大切です。
- ワイエルシュトラス方程式は五つの係数を持つ形。Leanはその係数を構造に保存します。
- 特異点のないワイエルシュトラス曲線に指定された点を伴わせると、楕円曲線になります。どんな係数でも特異点がないとは限りません。
小さな例で確かめる
一般の形はy² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆。フライ小包から特定の係数を用意します。
順番 27 / 64
高校
方程式で決まる曲線
方程式を満たす座標の組を集めたものが、ここでの曲線です。
まず、身近な例で
y=x²という式なら、(−2,4)、(0,0)、(2,4)などの点を選べます。式を満たす点を描くと曲線になります。FLTでは、y²やx³を使う別の式を扱います。
ちいさな確認：考えてみよう
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
x=2を入れるとx²=4でyと一致します。xとyが同じ数かではなく、方程式を満たすかを見ます。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
はい。 x=2を入れるとx²=4でyと一致します。xとyが同じ数かではなく、方程式を満たすかを見ます。
Leanの定義・原文の抜粋
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
このLeanの読み方
Rは係数の型。五つの欄がa₁・a₂・a₃・a₄・a₆を保存します。この構造だけで特異点がないと保証されるわけではありません。