大学
1の原始3乗根が入った世界では、三乗の和が三つの因子に分かれます。
5²−3²=(5+3)(5−3)のように、式を積に分けると調べやすくなります。三乗の証明では、ω³=1なのにω≠1となる数ωを使う世界へ進みます。普通の整数にはない数です。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
前者は8×2=16で25−9と一致。後者は4です。積に分けるときも、式の値を保ちます。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
(5+3)(5−3)。 前者は8×2=16で25−9と一致。後者は4です。積に分けるときも、式の値を保ちます。
普通の整数の世界では、x² − y² = (x + y)(x − y)という分解がおなじみです。環を豊かにする同じ贈り物が三乗の和にもやってきます。1の原始3乗根があるからこそ、三つの因子が現れるのです。
Mathlib · db584cd · Three.lean
/-- Given `S' : Solution'`, the key factorization of `S'.a ^ 3 + S'.b ^ 3`. -/lemma a_cube_add_b_cube_eq_mul :S'.a ^ 3 + S'.b ^ 3 = (S'.a + S'.b) * (S'.a + η * S'.b) * (S'.a + η ^ 2 * S'.b) := bysymmcalc _ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+η^3)+η^3*S'.b^3 := by ring_ = S'.a^3+S'.a^2*S'.b*(η^2+η+1)+S'.a*S'.b^2*(η^2+η+1)+S'.b^3 := bysimp [hζ.toInteger_cube_eq_one]_ = S'.a ^ 3 + S'.b ^ 3 := by rw [eta_sq]; ring
ここでλ := ζ₃ − 1は、アイゼンシュタイン整数環のノルム3の素元です。この環に素元がこれ一つしかない、という意味ではありません。降下法では、この選んだλがcを割る回数を測ります。表示の計算は因数分解を証明し、後の補題が互いに素という条件や割り切れる条件を使って因子を整理します。
アイゼンシュタインの世界の三つの因子
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
1の原始3乗根が入った世界では、三乗の和が三つの因子に分かれます。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
普通の整数の世界では、x² − y² = (x + y)(x − y)という分解がおなじみです。環を豊かにする同じ贈り物が三乗の和にもやってきます。1の原始3乗根があるからこそ、三つの因子が現れるのです。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →