『ベーシック圏論』で圏論の勉強をしているのですが、Set圏での随伴がカリー化と結びついているというトピックが色々な概念を含み、あとで随伴の復習をする際に便利な素材だと思いました。具体的には Set圏における関手 -×B とその右随伴である (-)ᴮ の構成を通じて Set がカルテシアン閉であることを確認します。
『ベーシック圏論』p49, p56, p110, p196 あたりのトピックをまぜこぜにしたような記事です。
表記
基本的に『ベーシック圏論』に準じます:
- SetはSet圏をあらわします
- 圏𝓐 とその対象 A,B について 表記 𝓐(A,B) は、AからBへの射の集合を表します。たとえば Set(B, C) は B→C なる関数集合を表します。
- 集合B,C にたいして Cᴮ で B→C なる関数集合 Set(B,C) を表します。集合の場合は三つの表記 Cᴮ, B→C, Set(B,C) は同じものを指します。
カリー化
2変数関数を、1変数関数に変換する操作をプログラミング言語ではカリー化と呼びます。例えば、足し算plusは2変数関数ですが、対応するカリー化された関数cplusを以下のように曖昧なく構成できて相互変換できます:
// plus をカリー化した cplus を簡単に構成できる
const plus = (x,y) => x + y;
const cplus = x => y => x + y;
// 足し算に限らず任意の2変数関数をカリー化・アンカリー化できる
const curry2 = f => x => y => f(x, y);
const uncurry2 = f => (x, y) => f(x)(y);
// カリー化関数を使ってカリー化した cp は cplus は関数としては同じ
const cp = curry2(plus);
集合の言葉にすると
上記の議論を集合の言葉で言うと
「A×B→C と A→Cᴮ との同型写像とその逆写像を構成した」
となります。A×B→C なる関数の例がplusで、 A→Cᴮ なる関数の例がcplusで、カリー化関数curry2: (A×B→C)→(A→Cᴮ) はそれらの同型写像です。逆写像はアンカリー化関数uncurry2です。
随伴をみつける
以上のように全てを Set内の射としてとらえるのも一つの見方ですが、別の見方をすることで随伴が見つかります。随伴があると思って先の式を少し書き直します:
Set(A×B, C) ≅ Set(A, Cᴮ)
すると Set→Set なる二つの関手 ×B と (-)ᴮ が見えてきます。なぜなら、それぞれに F,Gと名前をつけると
Set(F(A), C) ≅ Set(A, G(C))
となり随伴の定義である同型性と同じ見た目になるからです。Bを任意だが固定された集合とすると、FやGが具体的にどのような関手なのか（どのような関手を構成するべきか）は自明です。FとGが随伴であるためには、これに加えて自然性を満たすことを確かめる必要があります。つまり集合の言葉で言えば「二つの写像 A×B→C と A→Cᴮ とが上記関手で対応づくように、二つの合成写像 A×B→C→D と A→Cᴮ→Dᴮ とが対応する」、同様に「二つの写像 A→Cᴮ と A×B→C とが上記関手で対応づくように二つの合成写像 X→A→Cᴮ と X×B→A×B→C とが対応する」となりますが、これを満たすのはほぼ自明です（……それほど自明でもないという人がいるかもしれませんが具体例を考えればわかるはず……）。
随伴性による射の構成
『ベーシック圏論』p50. では随伴性を射の構成法とみなす記述があり、示唆に富んでいます。
射の配列 A₀→A₁→..→Aₙ, F(Aₙ)→B₀, B₀→B₁→..→Bₘ からちょうどひとつの射 A₀→G(Bₘ) を構成できる
これを、以上の議論に適用するとこのような言明になります:
「どれか一つの2変数関数を選ぶと、そのカリー化された関数をちょうどひとつ構成できる」
まあ、curry2をすでに構成してしまっているのでありがたみはない言明ですが、「関数を部分適用された世界」と「関数を全部適用（？）した世界」が随伴性によって並行して議論できるという感触が味わえます。
カルテシアン閉
以上の議論は、ひとことでいえば「Set はカルテシアン閉である」を丁寧に追っただけの話です。『ベーシック圏論』p197 の定義を引用すると
圏𝓐がカルテシアン閉とは, 𝓐が有限積を持ち, 各B∈𝓑について関手 ×B: 𝓐→𝓐 が右随伴―――(-)ᴮと表記する――を持つことをいう。
なお、𝓐(A×B,C) ≅ 𝓐(A,Cᴮ) が自然に成り立つことは随伴の定義から直接従います。
カルテシアン閉圏は、圏論的アプローチでプログラム意味論を展開する第一歩なので、Setをその具体例として確認しておいて損はなかったはず。