圏論ノート：随伴関手

いつもわからなくなるので随伴関手の復習をします。

随伴関手：定義

C, Dを圏、F: C → D、G: D → Cを関手とします。FがGの左随伴関手あるいはGがFの右随伴関手とは、まず

という全単射があり、さらにこの全単射がXとYについて自然であることです。Xについて自然とは、

はそれぞれ圏CからSetへの関手ですが、上の全単射がこの二つの関手の自然変換になっていることです。同様にYについて自然とは

はそれぞれ圏DからSetへの関手ですが、上の全単射がこの2つの関手の自然変換になっていることです。

FがGの左随伴関手になっているとき、F┨Gと書きます。

例：積集合とべき集合

集合Xに直積集合X×Zを割り当てる関手Fを考えます。また、集合Yにべき集合Y^Z（ZからYへの関数全体）を割り当てる関手Gを考えます。すると、FはGの左随伴関手です。Hom(X×Z, Y)の元fはXとZの値のペアを取ってYを返す関数fです。次にfに対してg(z) = f(x, z)を対応させる写像πを考えます。ここでzはZの元です。

πはHom(X×Z, Y)からHom(X, Y^Z)への写像です。f≠f'とするとあるx, zがあってf(x, z)≠f'(x, z)です。よって、対応するg(z)≠g'(z)です。つまりπは単射です。次にある写像h(x) = g ∊Y^Zを考えます。f(x, z):=h(x)(z)を考えます。π(f)=hです。よってπは全射です。

πの自然性は面倒（これだから圏論嫌い）なのでやりません。

この例はいわゆるカリー化になっています。つまり、2変数の関数fを1変数の関数を返す関数π(f)に変換しています。同じような議論が集合の圏だけでなくプログラミング言語の型と関数の作る圏でもできます。違いはプログラミング言語の世界ではHomは集合だけでなくそれ自体型だということです。そういう圏に名前があったような気がしますが忘れました。

まとめ

随伴関手の復習をして、カリー化が随伴性の一種であることを示しました。