大学院
局所環は極大イデアルを一つだけ持ち、その外はすべて可逆です。
普通の整数では5+(−4)=1ですが、5も−4も、整数の逆数を持ちません。局所環は、このようなことが起きない世界です。和が1なら、少なくとも片方は掛け算を元に戻す相手を持ちます。
上の具体例を見ながら考えよう。何度やり直しても大丈夫。
1/5も−1/4も整数ではありません。この例は、整数全体が表示した局所環の条件を満たさない理由になります。
この確認では、説明に合う答えを選べました。漫画の中でも、同じ考え方を探してみよう。
いいえ、どちらも整数の逆数を持たない。 1/5も−1/4も整数ではありません。この例は、整数全体が表示した局所環の条件を満たさない理由になります。
ℤは試験をくぐり抜けません:a = 5、b = −4はa + b = 1を満たし、どちらも単元ではありません——ℤの門は素数の数だけあります。ℓ進の世界ℤ_ℓは合格します:その元はℓで割れないとき限り可逆で、和が1になる組の一方は必ず門の外にいます。
Mathlib · db584cd · Defs.lean
/-- A semiring is local if it is nontrivial and `a` or `b` is a unit whenever `a + b = 1`.Note that `IsLocalRing` is a predicate. -/@[wikidata Q1142704]class IsLocalRing (R : Type*) [Semiring R] : Prop extends Nontrivial R whereof_is_unit_or_is_unit_of_add_one ::/-- in a local ring `R`, if `a + b = 1`, then either `a` is a unit or `b` is a unit. In anotherword, for every `a : R`, either `a` is a unit or `1 - a` is a unit. -/isUnit_or_isUnit_of_add_one {a b : R} (h : a + b = 1) : IsUnit a ∨ IsUnit b
classはNontrivialとisUnit_or_isUnit_of_add_oneをまとめます。可換環では、これは極大イデアルがちょうど一つあることに対応します。真のイデアルで割った商も局所環です。変形やパッチングの議論は局所環という仮定を明示的に使い、多項式環や任意の局所化が自動的に局所環になるわけではありません。
門が一つの環
まず「3段階で考えよう」を上から読みます。Leanの原文は、その後でも大丈夫です。
局所環は極大イデアルを一つだけ持ち、その外はすべて可逆です。
このページの「この言葉の前に」に、先に知ると読みやすい言葉があります。
ℤは試験をくぐり抜けません:a = 5、b = −4はa + b = 1を満たし、どちらも単元ではありません——ℤの門は素数の数だけあります。ℓ進の世界ℤ_ℓは合格します:その元はℓで割れないとき限り可逆で、和が1になる組の一方は必ず門の外にいます。
閉じれば、読んでいた場所に戻れます。このページに合わせて用意したヒントです。
最初の小さな物語から読む →