3段階で考えよう
- 余りの表現のデータを固定し、どんな持ち上げを認めるかを指定します。
- 環は足し算とかけ算のある計算の仕組み。変形環は、適切な他の環への写像で持ち上げを整理します。
- 普遍性は、条件に合う候補ごとに、整合する写像が一意に得られること。Leanの長い条件が「認める」の中身を指定します。
小さな例で確かめる
普遍的な注文書は、条件に合う持ち上げごとに写像を用意します。適当なサンドイッチを持ち上げとして受け取るわけではありません。
順番 58 / 64
大学院
変形環と普遍性
条件に合う持ち上げを、一つの代数的な対象からの写像で整理します。
まず、身近な例で
余り2だけなら、もとの数の候補は2、5、8など。もっと豊かな数学のデータにも、条件に合う持ち上げ方がいくつもあります。変形環は、その候補や写像をまとめて扱う仕組みです。好きな答えを選ぶものではありません。
ちいさな確認：考えてみよう
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
余りだけでは候補が残るように、持ち上げにも可能性があります。変形の問題では、許される候補や写像の条件を指定します。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
答えと考え方を読む
いいえ、指定した条件に合う持ち上げを扱う。 余りだけでは候補が残るように、持ち上げにも可能性があります。変形の問題では、許される候補や写像の条件を指定します。
Leanの定義・原文の抜粋
FLT · aa2d8b3 · Def_GaloisRep_DeformationRingData.lean
universal : ∀ (A : Type) [CommRing A] [IsLocalRing A] [IsNoetherianRing A][IsAdicComplete (IsLocalRing.maximalIdeal A) A] [Algebra 𝒪 A] [IsLocalHom (algebraMap 𝒪 A)],Function.Surjective (IsLocalRing.residue A ∘ algebraMap 𝒪 A) →∀ ρA : GaloisRepAdic A, 𝒟 ρA →ρA.residual.IsEquiv(ρbar.baseChangeAlong (IsLocalRing.ResidueField.map (algebraMap 𝒪 A))) →∃! φ : R →ₐ[𝒪] A, ∃ hφ : IsLocalHom (φ : R →+* A),
このLeanの読み方
これはDeformationRingDataのuniversal欄。∃!はφがちょうど一つ存在すること。→ₐ[𝒪]は指定された代数の構造を保つ写像です。