ブルバキ・ヴィットの定理

数学においてブルバキ・ヴィットの定理（ブルバキ・ヴィットのていり、テンプレート:Lang-en-short）は、半順序集合に関する基本的な不動点定理であり、ニコラ・ブルバキとエルンスト・ヴィットの名に因む。この定理は、$(X,⪯)$ が空でない半順序集合であって、任意の全順序部分集合に上限が存在するとき、

テンプレート:Math

が

$x\in X⟹f(x)⪰x$

を満たせば、テンプレート:Mvar は不動点を持つことを述べている。

有限な半順序集合の例

半順序集合 テンプレート:Mvar が有限であれば、定理の主張は簡単に理解でき、それが直接の証明となる。 テンプレート:Math を任意の元として、漸化式

テンプレート:Math

が定める点列 テンプレート:Math は単調増加である。テンプレート:Mvar は有限だから、この点列は、

十分に大きい テンプレート:Mvar に対して テンプレート:Math

で定常状態に至る。よって、テンプレート:Math は テンプレート:Mvar の不動点である。

定理の証明

テンプレート:Math を適当にとって固定し、順序数全体の類 テンプレート:Math の上の関数 テンプレート:Math を、

テンプレート:Math

テンプレート:Math

と再帰的に定義する。テンプレート:Math が極限順序数のときは、その定義の仕方から

テンプレート:Math

は、テンプレート:Mvar の中の全順序部分集合であるから、

テンプレート:Math

と定義する。テンプレート:Math は、単調増加関数である。仮に、テンプレート:Mvar が狭義単調増加であれば、テンプレート:Math から集合 テンプレート:Mvar の中への単射となり、ハルトークスの補題と矛盾する。順序数 テンプレート:Math について、テンプレート:Math であれば、

テンプレート:Math

である。

テンプレート:Math

とおけば、テンプレート:Math である。

適用事例

ブルバキ・ヴィットの定理には、重要な適用事例が幾つも存在する。選択公理からツォルンの補題を導く証明は、その最もよく知られた適用事案の一つである。ここでは、$(X,⪯)$ が空でない半順序集合であって、任意の全順序部分集合に上限が存在する場合について示す。

$(X,⪯)$ が極大元を持たないと仮定する。選択公理により、テンプレート:Mvar の空でない部分集合全体の集合 $𝔓(X)\setminus \{\mathrm{\varnothing }\}$ の選択関数 テンプレート:Mvar を取ることができる。テンプレート:Math だから、

$f(x)=g(\{y\in X\mid y\succ x\})(x\in X)$

により、関数 テンプレート:Math を定めることができる。テンプレート:Math ならば $f(x)\succ x$ だから、テンプレート:Mvar は不動点を持たないこととなり、定理に反する。

ツォルンの補題のこの特別な場合は、テンプレート:仮リンクの証明に用いられる。この原理は、任意の半順序部分集合において、任意の全順序部分集合を含む極大全順序部分集合が存在することを述べており、簡単に分かるようにツォルンの補題と同値である。

ブルバキ・ヴィットの定理は、他の適用事例も有する。特に、計算機科学において、計算可能関数の理論で用いる。また、領域理論では、再帰的データ型の定義に用いる。

参考文献

• テンプレート:Citation
• テンプレート:Citation