funlean.
順番 32 / 64

大学

ワイエルシュトラスの標準形

ここで使う曲線は、五つの係数で決まる標準の形に整えます。

まず、身近な例で

y²=x³−xを、x³+0x²−1x+0と書けば、どこにどの数が入るか分かります。一般のワイエルシュトラスの形には、五つの係数の欄があります。

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

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

x³+0x²−1x+0で、xにかかる係数は？

答えと考え方を読む

−1。 xの項は−1×xです。ここで0なのは、x²の係数と定数の欄です。

3段階で考えよう

  1. xとyの長い多項式の方程式は、いくつもの形を一度に隠していることがあります。そこでこの証明では、汎用性を保ったまま、形を一つの仲間に整えて扱います。
  2. 座標の変え方を選べば、適切な三次の方程式はy² + a₁xy + a₃y = x³ + a₂x² + a₄x + a₆と書けます。これがワイエルシュトラスの形です。
  3. 五つの係数は、一つの構造の名前のついた欄a₁・a₂・a₃・a₄・a₆に分けて保存します。それぞれ係数の型Rから取ります。

小さな例で確かめる

y² = x³ − xはこの形に合います。右辺をx³ + 0x² + (−1)x + 0と読んで、a₁ = a₂ = a₃ = 0、a₄ = −1、a₆ = 0です。

Leanの定義・原文の抜粋

Mathlib · db584cd · Weierstrass.lean

/-- A Weierstrass curve `Y² + a₁XY + a₃Y = X³ + a₂X² + a₄X + a₆` with parameters `aᵢ`. -/@[ext]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は係数がどの種類の数から来るかを宣言します。この構造はデータだけを持ちます。

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

この言葉を使う章

5. あやしい小包
わからない・道に迷った

ミカのたすけ舟

ワイエルシュトラスの標準形

今は、一つだけ

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

言葉をほどこう

ここで使う曲線は、五つの係数で決まる標準の形に整えます。

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

小さな手がかり

y² = x³ − xはこの形に合います。右辺をx³ + 0x² + (−1)x + 0と読んで、a₁ = a₂ = a₃ = 0、a₄ = −1、a₆ = 0です。

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

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