持ち上げ

追加条件のある定理で、余りの情報から元の豊かな情報へ進みます。

まず、身近な例で

3で割った余りが2。もとの数は2、5、8、11のどれでしょう？余りだけでは決まりません。「6より大きく10より小さい」という条件を付けてみよう。

数や条件を動かしてみよう

余りだけでは選べません。この先にも同じ余りの数が続きます。

この例と、本当の定義の違い

「6と10の間」は模型だけの条件で、持ち上げ定理の仮定ではありません。本当の定理は表現についてのもので、それぞれの仮定をすべて確かめます。

問いの数と、今動かしている図の数を見比べよう。何度やり直しても大丈夫。

3で割った余りが2なら、もとの数は必ず8？

答えと考え方を読む

いいえ、2、5、8、11などが候補。追加条件を外すと、図の四つとも余り2。「6 < n < 10」という模型の条件で8が残ります。本物の持ち上げには、その定理の仮定が必要です。

整数の余りが5を法として2でも、元が2・7・12のどれかは分かりません。持ち上げには追加の構造が不可欠です。

FLT · aa2d8b3 · S_WeierstrassCurve_modularity_of_semistableModel.lean

174    exact isModular_map_of_mlc1175      (liftingAtConductor_three_of_level_hns 3 rfl W hΔ hW h3 M₃ hres₃ hns₃ hcube₃)

これは一般的な逆操作の定義でなく、定理の適用例です。集めた証拠をliftingAtConductor_three_of_level_hnsへ渡しています。