大学院
曲線のデータと形式のデータが、余りの世界の中で一致することを一つの主張にまとめます。
13と18の差は5なので、5で割ると両方とも余り3。表現の定義でも、決められた余りの世界で算術の情報を比べます。もとの値が等しい、という意味ではありません。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
18−13=5です。差が5で割り切れるので余りは同じですが、もとの数は違います。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
いいえ。 18−13=5です。差が5で割り切れるので余りは同じですが、もとの数は違います。
13と18は5で割るとどちらも余り3。差が5だからです。定義では、選んだイデアル𝔪を法として算術のデータを比べます。余りで一致しても、元の値が等しいとは限りません。
FLT · aa2d8b3 · Def_FLTPrelim_ModularRep.lean
def ModularRepOfLevel (P : FreyPackage) (N : ℕ) : Prop :=∃ (f : CuspForm (CongruenceSubgroup.Gamma0 N) 2) (W : WeierstrassCurve ℤ)(𝔪 : Ideal (integralClosure ℤ ℂ)),f.IsNormalizedEigenform ∧ W.IsIntegralModelOf P.freyCurve ∧𝔪.IsMaximal ∧ (P.p : integralClosure ℤ ℂ) ∈ 𝔪 ∧∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → ¬ ℓ ∣ N → ℓ ≠ P.p →∃ a : integralClosure ℤ ℂ, (a : ℂ) = ModularFormClass.qCoeff f ℓ ∧a - ((W.apOfModel ℓ : ℤ) : integralClosure ℤ ℂ) ∈ 𝔪
∃は証人f・W・𝔪を求め、∧が条件を結びます。IsNormalizedEigenformとIsIntegralModelOfは、それぞれの前提のページを参照しています。
形式と表現をつなぐ
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
曲線のデータと形式のデータが、余りの世界の中で一致することを一つの主張にまとめます。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
13と18は5で割るとどちらも余り3。差が5だからです。定義では、選んだイデアル𝔪を法として算術のデータを比べます。余りで一致しても、元の値が等しいとは限りません。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →