3段階で考えよう
- 曲線は条件に合う素数で算術の数を与えます。形式は同じ素数で係数を与えます。
- モジュラー性は、定義が求める場所で両者が正確に一致する、条件つきの正規化された形式の存在を求めます。
- 正のレベルの存在も必要です。相方があることは定理で示すもので、楽器を二つ描けば得られるわけではありません。
小さな例で確かめる
二重奏の対応は、指定された良い素数でのqCoeff f p = apOfModel W pという正確な等式です。
順番 51 / 64
大学
曲線のモジュラー性
曲線の算術データと係数が一致する、条件つきの形式を見つけること。
まず、身近な例で
同じものを別々の方法で調べた二人が、2、−1、4という数の並びを記録しました。場所を選んで、二つの記録を比べよう。
1番目は、どちらも2。少しの一致だけで定理全体を確かめたことにはなりません。
この例と、本当の定義の違い
この3個の数は比べ方を示す架空の模型です。実際のモジュラー性には、条件を満たす形式と必要な対応全体が必要で、3か所の一致では足りません。
ちいさな確認：考えてみよう
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
図の記録の場所を変えてみよう。これは比べ方を見せる架空の数で、条件に合う形式の存在や定理全体を示すものではありません。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ、本物の対象と必要な対応全体が要る。 図の記録の場所を変えてみよう。これは比べ方を見せる架空の数で、条件に合う形式の存在や定理全体を示すものではありません。
Leanの定義・原文の抜粋
FLT · aa2d8b3 · Def_FLTPrelim_Modularity.lean
def IsModularModelOfLevel (W : WeierstrassCurve ℤ) (N : ℕ) : Prop :=∃ f : CuspForm (CongruenceSubgroup.Gamma0 N) 2, f.IsNormalizedEigenform ∧∀ p : ℕ, p.Prime → W.IsGoodPrimeFor p → ¬ p ∣ N →ModularFormClass.qCoeff f p = (W.apOfModel p : ℂ)def IsModularModel (W : WeierstrassCurve ℤ) : Prop :=∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel Ndef IsModular (E : WeierstrassCurve ℚ) : Prop :=∃ W : WeierstrassCurve ℤ, W.IsIntegralModelOf E ∧ W.IsModularModel
このLeanの読み方
∃ fで形式を用意し、∧で条件を束ね、∀ pで素数を指定し、最後の=で一致を求めます。次の定義が正のレベルNを用意します。