scrap:ラムダ計算の自然性とお絵描き
http://www.chimaira.org/img5/wire-tensor-exp.png
モノイド閉圏Cには、モノイド積と指数が備わっているのでした。これらの演算は、二項関手〈双関手〉になります。
モノイド積二項関手 $ (-⊗ -):C×C→C
指数二項関手 $ [-,-] :C^\mathrm{op}×C→C
モノイド積は共変-共変の二項関手、指数は反変-共変の二項関手です。ただし、どっちの変数が反変になるかは書き方に依存します*1。例えば、指数形式 XA を中置演算子記号で X^A と書くと約束すると、
(-^-):C×Cop→C
です。この記事では、$ XA = [A, X] とAを左に書くので、第一変数〈左変数〉に関して反変です。
Cがモノイド閉圏であるためには、次の条件が必要です。
任意の対象 A∈|C| が定義する関手 (-⊗ A) と $ [A, -] は随伴ペアになる。
随伴を正確に記述するために、随伴系を「随伴に関する注意事項」に従って書くとすれば、次の随伴系〈adjunction | adjoint system〉があります。
$ (η, ε: (-⊗ A) -| [A, -], (-⊗ A):C→C)
この随伴系を、指数随伴系〈exponential adjunction〉とかテンソル・ホム随伴系〈tensor-hom adjunction〉と呼びます。「テンソル・ホム」の由来は； テンソル積はモノイド積と同義に使われることがあり、ホムは内部ホム、つまり指数です。「テンソル・ホム」は「モノイド積と指数のあいだの」という形容詞です。
Cの対象 X, Y を選んで、指数随伴系が導くホムセット間同型を書けば：
$ C(X⊗ A, Y) ≅ C(X, [A, Y])
この同型を与える左から右方向の写像をカリー化〈currying〉と呼び、Λで書くことにします。
$ Λ:C(X⊗ A, Y)→C(X, [A, Y])
随伴系の定義より、Λには逆写像が存在します。Λ-1を反カリー化〈uncurrying〉と呼びます*2。
cripped at 2020/04/07 12:11