直積関手からの普遍射

考える圏を S とする。
S のある対象 A に対して S の任意の対象 Z との直積 A × Z が存在するとする。このとき、A と直積をとる操作は S から S への関手になっている:

A×-: S → S

この直積関手から S の対象 X への普遍射を考える。すなわち、S のある対象 X^A と射 ev: A×X^A → X があり以下の性質を満たすとする。

条件
S の任意の対象 B と任意の射 f: A×B → X に対して、右の三角の図式を可換にするような唯一の射 f~: B → X^A が存在する。

   B          A×B 
   │          │ ＼
   │          │   ＼
 f~│     A×f~│     ＼ f
   │          │       ＼
   │          │         ＼
   ↓          ↓           ┘
   XA         A×XA ────→ X
                        ev

対象をベキの形に書いたこと、射を ev と呼ぶことには特に意味はなく、慣習に従っただけである。

この性質を満たす X^A と ev の組を、「直積関手 A×- から X への普遍射」という。
上のように直積関手からの普遍射が存在する場合、対象 X^A をベキ対象(power object)、射 ev を 評価射(evaluation map) と呼ぶのが普通である。ベキ対象 X^A は、A から X への射(関数)の集まり、ev は(関数)適用とみなせることが多い。

普遍射の性質から、射 f: A×B → X に対して唯一つ射 f~: B → X^A が対応し、逆の対応も存在する。従って f と f~ の対応は一対一(全単射)になっている。f~ のことを「f の (exponential) transpose」と呼ぶことがある。

で、transpose は、僕にはカリー化に見えるんだよなぁ。