雑記帳
カントールの対角線論法を圏論的に俯瞰する【ローヴェアの不動点定理 (Lawvere's fixed-point theorem)】
ローヴェアの不動点定理 (Lawvere's fixed-point theorem)
定理の内容
任意のカルテシアン閉圏において、 point-surjective である射 \(\phi:A\rightarrow B^A\) が存在するならば、任意の射 \(f:B\rightarrow B\) は不動点 \(s:1\rightarrow B\) を持つ。
※一応英語版 Wikipedia でもこの定理が紹介されているので信憑性を疑う場合は是非チェックを。(ちなみに Wikipedia では「point-sujective」ではなく「弱 point-surjective (weakly point-surjective)」に対して一般に成り立つことを Lawvere の不動点定理としているが、ここでは nLab の流儀に従っておく。)
証明
\(f:B\rightarrow B\) を任意の射、\(q:1\rightarrow B^A\) を \(\lambda[{\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f]\) として定義される \(B^A\) の大域要素とする。
この時 \(\phi:A\rightarrow B^A\) が point-surjective であることを仮定しているので、point-surjective の定義より、\(\phi\) によって \(q\) へとうつされる \(A\) の大域要素 \(p:1\rightarrow A\) (つまり \(p {\sf \, ⨟ \,} \phi = q\) を満たす \(p\)) の存在が従う。
こうして得られる射の組み合わせとして構成される射である
\[
s = \langle p {\sf \, ⨟ \,} \phi , p \rangle {\sf \, ⨟ \,} {\rm ev}
\]
は、\(f\) の不動点となる。
以下具体的に確認をすると、
\[
\begin{align}
s &= \langle p {\sf \, ⨟ \,} \phi , p \rangle {\sf \, ⨟ \,} {\rm ev} \\
&= \langle q , p \rangle {\sf \, ⨟ \,} {\rm ev} \\
&= \langle \lambda[{\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f] , p \rangle {\sf \, ⨟ \,} {\rm ev} \\
&= \langle B^A {\sf \, ⨟ \,} \lambda[{\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f] , p {\sf \, ⨟ \,} A \rangle {\sf \, ⨟ \,} {\rm ev} \\
&= \langle B^A , p \rangle {\sf \, ⨟ \,} (\lambda[{\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f]\times A) {\sf \, ⨟ \,} {\rm ev} \\
&= \langle B^A , p \rangle {\sf \, ⨟ \,} ((\lambda[{\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f]\times A) {\sf \, ⨟ \,} {\rm ev}) \\
&= \langle B^A , p \rangle {\sf \, ⨟ \,} ({\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f) \\
&= \langle B^A , p \rangle {\sf \, ⨟ \,} {\rm prj}_2 {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= (\langle B^A , p \rangle {\sf \, ⨟ \,} {\rm prj}_2) {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= p {\sf \, ⨟ \,} \Delta {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= (p {\sf \, ⨟ \,} \Delta) {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= \langle p,p \rangle {\sf \, ⨟ \,} (\phi \times A) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= (\langle p,p \rangle {\sf \, ⨟ \,} (\phi \times A)) {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= \langle p {\sf \, ⨟ \,} \phi,p {\sf \, ⨟ \,} A \rangle {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= \langle p {\sf \, ⨟ \,} \phi,p \rangle {\sf \, ⨟ \,} {\rm ev} {\sf \, ⨟ \,} f \\
&= (\langle p {\sf \, ⨟ \,} \phi,p \rangle {\sf \, ⨟ \,} {\rm ev}) {\sf \, ⨟ \,} f \\
&= s {\sf \, ⨟ \,} f \\
\end{align}
\]
即ち
\[
s {\sf \, ⨟ \,} f = s
\]
つまり、\(f\) に大域要素 \(s\) を入力すると、再び \(s\) を出力することが圏論的に示された。
用途・応用
不動点コンビネータが定める不動点への意味付け
(..)
対象とその冪対象の間を結ぶエピック射の存在
point-surjective の概念は一般にはエピックと直接的な繋がりがないが、後ほど登場するトポスと呼ばれる圏においてはそれらの概念はぴったりと重なり、同値な概念として扱われることになる。
トポスでは冪対象と呼ばれる特別な種類の指数対象が構成されるのだが、この時、「任意の対象について、その対象からその対象の冪対象へのエピック射は存在するのか (考えているトポスでカントールの定理が成立するのか)」ということを、この定理を使って考察することができる。
因みに「カントールの対角線論法 (Cantor's diagonal argument)」の Wikipedia 記事で、「対角線論法の関数による表現」として紹介されている説明は混乱しやすい記述になっていて少しわかりづらいが、その論法を使ったカントールの定理の証明は本質的には
- ETCS 集合論において、何らかのエピック射 \(\psi:X\rightarrow \Omega^X\) が存在すると仮定すると、任意の自己準同形 \(\Omega\rightarrow\Omega\) が不動点を持たなければいけないわけだが、例えば否定 \((\neg):\Omega\rightarrow\Omega\) (具体的な構成方法は「置換公理型を認めない初等トポスの一般論の中で、集合 {x∈X|P(x)} はどのようにして構成されるのか」を参照) は不動点を持たないため、その仮定は矛盾する。
といった感じの話であり、このようにローヴェアの不動点定理を明示的に持ち出してくることによって非常にわかりやすい記述に書き変わる。
タグ一覧: