Adámekの不動点定理を比較的わかりやすく解説してみる

nLabの記事（terminal coalgebra for an endofunctor in nLab）を読んでいたら、図式は読みづらいし行間は広いしで、読解にだいぶ時間を使った。せっかくなので、quiver（図式を簡単に描けるアプリケーション）の練習と埋め込み機能のテストを兼ねて¹、大部分を参考にしながら自分なりにまとめ直すことにした。

自分用のメモみたいなもんなので、あんまりクオリティとか正確性に自信はない……

nLabの方ではterminal coalgebraについての定理だが、こっちではinitial algebraのバージョンについて書く。

Adámekの不動点定理

initial object \( 0 \) を持つ圏 \( C \)と、その上の自己関手 \( F \) を考える。\( F \) はcolimitを保つとし、以下のchainがcolimit \( T \) を持つとする。

このとき、射 \( \theta \colon FT \to T \) が存在して、\( (T, \theta) \) はinitial algebraとなる。

証明

まず、\( T \) がcolimitであったから、次のようなcoconeがとれる。

このcocone全体を \( F \) で送って \( 0 \) からの射を左下にくっつけると、次のようになる。

すると、\( F \) がcolimitを保つという条件から、このcoconeもchainのcolimitを与える。colimitの一意性より \( FT \cong T \) となるから、この同型射を \( \theta \colon FT \to T \) とする。

algebra \( (T, \theta) \) が得られたので、これのinitialityを証明するために、任意にalgebra \( (A, \alpha) \) をとる。

射の族 \( f_n \colon F^n 0 \to A \) を、以下のように帰納的に定義する。

$$ \begin{align*} f_0 & \text{は、一意射} \\ f_{n+1} &= \alpha \circ Ff_n \end{align*} $$

すると、これはchainについてcoconeになる。すなわち、\( f_n = f_{n+1} \circ F^n! \) となる。

これは、以下のように帰納法により確かめられる（nLabの記事では"It is easily checked by induction"とされていたが、全然easyではないと思う！）。

まず、\( f_0 \) についてはいいだろう。（一意であるため）

次に、\( f_n = f_{n+1} \circ F^n! \) を仮定して、\( f_{n+1} \) について示す。

以下の図式を考えると、これは可換になる（左下の三角形は定義から、右上の三角形は仮定から）。

この図式全体を \( F \) で送り、もとの図式と合わせて以下の可換図式を得る。

これの真ん中部分だけを取り出すと、次のようになる。

見やすいように形を整えて、定義から可換となるような射を追加すると、以下の通り。

よって、示された。

さて、これによって \( (A, f) \) がchainのcoconeであることがわかった。colimitの普遍性から、一意に射 \( h \colon T \to A \) が存在して、以下の図式が可換になる。

ここからゴチャゴチャしてくるので、図式の一部分だけを切り取って載せることにするが、常に考えているのはcocone全体である。

これをさらに \( F \) で送ったものを考えると、\( T \) の普遍性から、以下の図式が可換になる。

さらに、\( f_n \) の定義から、以下が可換になる。

よって、\( \alpha \circ Fh \circ \theta^{-1} \) はcoconeの間の射なので、一意性より以下の図式が可換になる。

すなわち、\( h \) は \( (T, \theta) \) から \( (A, \alpha) \) への一意なalgebra mapである。 \( \blacksquare \)

おわりに

証明が間違っていたりしたら教えてください。