大学院
イデアルの上昇列は必ず止まります。環の内側に無限の塔はありません。
16の倍数の集まりは8の倍数に入り、次は4、次は2と集まりが広がります。ネーター性は、イデアルという特別な集まりをこの向きに増やすと、いつか増加が止まる性質です。イデアルには計算の規則もあります。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
16k=8×(2k)です。一方、8は8の倍数ですが16の倍数ではありません。集まりが広がる向きを確かめよう。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
16の倍数は8の倍数にも入る。 16k=8×(2k)です。一方、8は8の倍数ですが16の倍数ではありません。集まりが広がる向きを確かめよう。
ℤの塔(16) ⊂ (8) ⊂ (4) ⊂ (2)——8が16を割るので16は8の倍数の中に置きます——は必ず止められ、実際止まります:ℤのイデアルはどれも一つの数が生成するから、上昇列は有限のステップで終わります。
Mathlib · db584cd · Defs.lean
/-- A (semi)ring is Noetherian if it is Noetherian as a module over itself,i.e. all its ideals are finitely generated. -/@[wikidata Q582271]abbrev IsNoetherianRing (R) [Semiring R] :=IsNoetherian R Rtheorem isNoetherianRing_iff {R} [Semiring R] : IsNoetherianRing R ↔ IsNoetherian R R :=Iff.rfl/-- A ring is Noetherian if and only if all its ideals are finitely-generated. -/theorem isNoetherianRing_iff_ideal_fg (R : Type*) [Semiring R] :IsNoetherianRing R ↔ ∀ I : Ideal R, I.FG :=
略記の設計はMathlibの作法の見本です:読める概念に名前を付け、加群側の条件で実現し、そして頭の中にある生成元の数え方との等価性を証明する(isNoetherianRing_iff_ideal_fg)。鎖の安定化や二次元の定理がこのファイルの残りを満たします。頂上の仮定の列では略記のまま現れます——述べるのは短く、稼ぐのは重い。
いつまでも育たない環
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
イデアルの上昇列は必ず止まります。環の内側に無限の塔はありません。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
ℤの塔(16) ⊂ (8) ⊂ (4) ⊂ (2)——8が16を割るので16は8の倍数の中に置きます——は必ず止められ、実際止まります:ℤのイデアルはどれも一つの数が生成するから、上昇列は有限のステップで終わります。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →