3段階で考えよう
- 局所的な部品の仕組みを集めます。各部品には代数的な条件があります。
- 関連する部品どうしの一致も指定します。個別に正しいデータでも、つながらないことがあります。
- すべての仮定のもとで、一つの整合した対象を作るのがパッチングの定理。持ち上げに貢献する構成で、これだけがモジュラー性の証明全体ではありません。
小さな例で確かめる
正しい布切れの山だけではキルトは完成しません。端の接続条件も入力の一部です。
順番 61 / 64
大学院
パッチング
部品だけでなく接続の条件もそろえ、一つの対象を作ります。
まず、身近な例で
地図の切れ端がそれぞれ正しくても、同じ道のつなぎ目が合わなければ一枚にできません。数学のパッチングでも、部品ごとの正しさと、対応する部分の整合性が必要です。
ちいさな確認：考えてみよう
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
同じ道を重ねてみよう。つなぎ目の情報が合う必要があります。証明でも、定められた整合性の条件を用意します。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ、重なる部分の整合性も必要。 同じ道を重ねてみよう。つなぎ目の情報が合う必要があります。証明でも、定められた整合性の条件を用意します。
Leanの定義・原文の抜粋
FLT · aa2d8b3 · Def_Algebra_PatchingDatum.lean
structure Algebra.PatchingDatum (𝒪 : Type) [CommRing 𝒪] (ℓ r : ℕ) (R : Type) [CommRing R][Algebra 𝒪 R] (M : Type) [AddCommGroup M] [Module R M] : Type 1 wherelevel : ∀ n : ℕ, Algebra.PatchingLevel 𝒪 r R M(Ideal.span (Set.range fun j : Fin r =>((1 + MvPowerSeries.X j) ^ (ℓ ^ n) - 1 : MvPowerSeries (Fin r) 𝒪)))
このLeanの読み方
levelはnごとのデータを用意します。PatchingLevel自体が代数的な条件を持っています。構造を持つ入力で、適当なのりではありません。