funlean.
順番 56 / 64

大学院

離散付値環

主イデアル環で局所、しかも体ではない環:本物の門と一つの物差しの元。

まず、身近な例で

8=2³には2が3回、12=2²×3には2が2回入っています。決めた因子が何回入るかで測るのが、付値を考える入口。離散付値環では、この測り方に正確な規則があります。

ちいさな確認：考えてみよう

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

12=2²×3には、因子2が何回入っている？

答えと考え方を読む

2回。 2で割ると12→6→3で2回。残りの3は2で割り切れません。これが付値を考える小さな例です。

3段階で考えよう

  1. 離散付値環とは、三つの資格証明を一度に持つ整域です:すべてのイデアルが一つの生成元の倍数であること(主イデアル環)、世界が局所であること(門が一つ)、それでいて体ではないこと——門が本物: maximalIdeal R ≠ ⊥。
  2. 極大イデアルを生成する素元π（一様化元）を一つ選びます。0ではない元は、自然数n ≥ 0について単元 × π^nと表せます。0にはこの有限の形はなく、付値の言葉では無限大として扱います。前のλの回数も、このような割り切れ方の物差しの例です。
  3. R = Tの主張での頂上の世界𝒪は離散付値環です:仮定の列に[IsDomain 𝒪]と[IsDiscreteValuationRing 𝒪]が並びます。局所で主イデアルとは、ただ一つの測れる傷——変形環を比べ、つなぎパッチを当てるための言葉です。

小さな例で確かめる

アイゼンシュタイン整数環そのものは局所環ではありません。λが生成する素イデアルで局所化すると離散付値環になり、λが物差しになります。0ではないcをλが割る回数は、三乗の場合の候補の順位づけに使う付値の例です。

Leanの定義・原文の抜粋

Mathlib · db584cd · Basic.lean

/-- An integral domain is a *discrete valuation ring* (DVR) if it's a local PID which  is not a field. -/class IsDiscreteValuationRing (R : Type u) [CommRing R] [IsDomain R] : Prop    extends IsPrincipalIdealRing R, IsLocalRing R where  not_a_field' : maximalIdeal R ≠ ⊥

このLeanの読み方

IsPrincipalIdealRingはイデアルが一つの元で生成されること、IsLocalRingは極大イデアルが一つであることを表します。not_a_field'はそのイデアルが0ではないという条件です。極大イデアルの生成元を一様化元と呼び、有限の累乗と単元の積で表す説明は0ではない元に適用します。

元の原文 ↗ · L56–60保存した原文全体を開く

この言葉を使う章

12. 二つの工房、同じ注文13. ピップの無謀なキルト
わからない・道に迷った

ミカのたすけ舟

離散付値環

今は、一つだけ

まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。

言葉をほどこう

主イデアル環で局所、しかも体ではない環:本物の門と一つの物差しの元。

このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。

小さな手がかり

アイゼンシュタイン整数環そのものは局所環ではありません。λが生成する素イデアルで局所化すると離散付値環になり、λが物差しになります。0ではないcをλが割る回数は、三乗の場合の候補の順位づけに使う付値の例です。

閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。

最初の小さな物語から読む →