大学
余りの世界へ移した算術データが、形式の係数と一致すること。
二つの記録に8と5があります。数は違っても、3で割ると両方とも余り2。片方の数を動かすと、いつ余りがそろうかな？
左の余り2、右の余り2。そろいました。
この二つの整数は、比べ方だけの模型です。実際には、条件を満たす形式の存在と、定められた算術の対応が必要。一組の余りが合うだけでは証明になりません。
問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。
図で8 ÷ 3と5 ÷ 3を比べよう。余りにすると元の情報の一部を失います。この一組だけで残余モジュラー性を証明したわけでもありません。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
余りは一致するが、もとの値は違う。 図で8 ÷ 3と5 ÷ 3を比べよう。余りにすると元の情報の一部を失います。この一組だけで残余モジュラー性を証明したわけでもありません。
普通の計算では7 − 2が5の倍数。定義では、二つの値の差がpを含むイデアル𝔪に入ることを求めます。
FLT · aa2d8b3 · Def_FLTPrelim_ModularRep.lean
def IsResiduallyModularOfLevel (W : WeierstrassCurve ℤ) (p M : ℕ) : Prop :=∃ (f : CuspForm (CongruenceSubgroup.Gamma0 M) 2) (𝔪 : Ideal (integralClosure ℤ ℂ)),f.IsNormalizedEigenform ∧ 𝔪.IsMaximal ∧ (p : integralClosure ℤ ℂ) ∈ 𝔪 ∧∀ ℓ : ℕ, ℓ.Prime → W.IsGoodPrimeFor ℓ → ¬ ℓ ∣ M → ℓ ≠ p →∃ a : integralClosure ℤ ℂ, (a : ℂ) = ModularFormClass.qCoeff f ℓ ∧a - ((W.apOfModel ℓ : ℤ) : integralClosure ℤ ℂ) ∈ 𝔪def IsResiduallyModular (W : WeierstrassCurve ℤ) (p : ℕ) : Prop :=∃ M : ℕ, 0 < M ∧ W.IsResiduallyModularOfLevel p M
𝔪はpを含む極大イデアルとして用意します。最後の「差 ∈ 𝔪」が余りでの一致。IsResiduallyModularがさらに正のレベルを求めます。
残余モジュラー性
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
余りの世界へ移した算術データが、形式の係数と一致すること。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
普通の計算では7 − 2が5の倍数。定義では、二つの値の差がpを含むイデアル𝔪に入ることを求めます。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →