3段階で考えよう
- 曲線は素数ごとに違うふるまいをします。導手は悪い還元の情報を、重複度も含めて記録します。
- 半安定曲線ではその寄与が制限されます。ここでの定義は、Δを割るすべての素数が選んだレベルを割ることを求めます。
- 素因子を取り除くレベル下げには、さらに証明済みの局所条件が必要。好きな因子を消す操作ではありません。
順番 57 / 64
大学
導手とレベル下げ
注意すべき素数を記録し、証明済みの条件でレベルの素因子を制限します。
まず、身近な例で
2×3×5なら素数のラベルが三種類、2²×3なら重なりもあります。導手も、素数ごとの情報を指数付きで記録します。気に入らないラベルを勝手に外せるわけではありません。
ちいさな確認：考えてみよう
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
ラベルは算術の情報を記録します。外すには必要な条件を証明します。手で荷札を貼り替えるだけでは、数学の結論は得られません。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ、定理が要求する条件の根拠が必要。 ラベルは算術の情報を記録します。外すには必要な条件を証明します。手で荷札を貼り替えるだけでは、数学の結論は得られません。
Leanの定義・原文の抜粋
FLT · aa2d8b3 · Def_FLTPrelim_ModularRep.lean
def IsModularModelOfConductorLevel (W : WeierstrassCurve ℤ) : Prop :=∃ N : ℕ, 0 < N ∧ W.IsModularModelOfLevel N ∧∀ ℓ : ℕ, ℓ.Prime → (ℓ : ℤ) ∣ W.Δ → ℓ ∣ N
このLeanの読み方
これはモジュラーモデルの導手レベルの条件の定義で、導手不変量そのものの完全な定義ではありません。最後の行が、Δを割る各素数はレベルも割るという条件です。