Cartesian Closed Category の定義。
初めての記事だよ。
cartesian closed category (CCCと略される)とは直感的には、object$X,Y$に対しその間の射の空間$[X\rightarrow Y]$も再びobjectとして扱えるcategoryのことである。もちろんobject$[X\rightarrow Y]$は、射の空間と見なされるに十分ないくつかの構造・操作、例えばカリー化やアンカリー化などをサポートするべきである。
以下、CCCの同値な定義を3つ書いて、終わり。
$\mathcal{C}$をfinite productを持つcategoryとする。
$\mathcal{C}$のobject$A,B$に対しobject$B^A$と射$e_{B,A}:B^A\times A\rightarrow B$が次の条件を満たすとき、組$(B^A,e_{B,A})$は$B$の$A$によるexponentialと呼ばれる。
条件：任意のobject$C$と射$f:C\times A\rightarrow B$に対し、ある射$f^*:C\rightarrow B^A$が一意に存在して$e_{B,A}\langle f^*p_{C,A}, q_{C,A}\rangle=f$が成立する。ただし$p_{C,A},q_{C,A}$はbinary productからの射影とする。
$\mathcal{C}$が任意のobject$A,B$に対し、$B$の$A$によるexponential$(B^A,e_{B,A})$を持つとき、$\mathcal{C}$はcartesian closed categoryと呼ばれる。
$\mathcal{C}$をfinite productを持つcategoryとする。
このとき任意のobject$A$に対し、自己関手$(-)\times A:\mathcal{C}\rightarrow\mathcal{C}$が伸びる。
任意のobject$A$について$(-)\times A$が右随伴$(-)^A$を持つとき、$\mathcal{C}$はcartesian closed categoryと呼ばれる。
cartesian closed categoryとは10個組$(\mathcal{C},T,\wedge,\supset,o,p,q,e,\langle\rangle,{}^*)$であって、以下の条件を満たすものを言う。
$\mathcal{C}$はcategory。
$T$は$\mathcal{C}$のobject。
$\wedge, \supset$はそれぞれ、$\mathcal{C}$のobjectの組$(A,B)$を受け取ってobject$A\wedge B$, $A\supset B$を与える演算。
$o$は$\mathcal{C}$のobject$A$を受け取って射$o_A:A\rightarrow T$を与える割り当て。
$p,q,e$はそれぞれ、$\mathcal{C}$のobjectの組$(A,B)$を受け取って射$p_{A,B}:A\wedge B\rightarrow A, q_{A,B}:A\wedge B\rightarrow B, e_{A,B}:(B\supset A)\wedge B\rightarrow A$を与える割り当て。
$\langle\rangle$は$\mathcal{C}$のdomainを同じくする射の組$(f:A\rightarrow C,g:A\rightarrow D)$を受け取って、射$\langle f,g\rangle:A\rightarrow C\wedge D$を与える演算。
${}^*$は$\mathcal{C}$の射$f:C\times B\rightarrow A$を受け取って、射$f^*:C\rightarrow B\supset A$を与える演算。
以下の等式が成立する。
- $f=o_A$ for any $f:A\rightarrow T$
- $p_{A,B}\langle f,g\rangle=f$
- $q_{A,B}\langle f,g\rangle=g$
- $\langle p_{A,B}h, q_{A,B}h\rangle=h$
- $e_{A,B}\langle f^*p_{C,B}, q_{C,B}\rangle=f$
- $(e_{A,B}\langle hp_{C,B}, q_{C,B}\rangle)^*=h$
私のオススメは3つ目です。
現在図式の類を一切載せていないのですが、Mathlog運営曰くxypicが導入される予定らしいので、そうしたら載せるかもしれない。可換図式だけでなく証明図を描けるやつもサポートしてほしいわね。
