Cartesian Closed Category の定義。

初めての記事だよ。

cartesian closed category (CCCと略される)とは直感的には、object $X, Y$ に対しその間の射の空間 $[X \to Y]$ も再びobjectとして扱えるcategoryのことである。もちろんobject $[X \to Y]$ は、射の空間と見なされるに十分ないくつかの構造・操作、例えばカリー化やアンカリー化などをサポートするべきである。

以下、CCCの同値な定義を3つ書いて、終わり。

人間に優しい定義

$C$ をfinite productを持つcategoryとする。

$C$ のobject $A, B$ に対しobject $B^{A}$ と射 $e_{B, A} : B^{A} \times A \to B$ が次の条件を満たすとき、組 $(B^{A}, e_{B, A})$ は $B$ の $A$ によるexponentialと呼ばれる。

条件：任意のobject $C$ と射 $f : C \times A \to B$ に対し、ある射 $f^{*} : C \to B^{A}$ が一意に存在して $e_{B, A} ⟨ f^{*} p_{C, A}, q_{C, A} ⟩ = f$ が成立する。ただし $p_{C, A}, q_{C, A}$ はbinary productからの射影とする。

$C$ が任意のobject $A, B$ に対し、 $B$ の $A$ によるexponential $(B^{A}, e_{B, A})$ を持つとき、 $C$ はcartesian closed categoryと呼ばれる。

圏論に馴れている人向けの定義

$C$ をfinite productを持つcategoryとする。

このとき任意のobject $A$ に対し、自己関手 $(-) \times A : C \to C$ が伸びる。

任意のobject $A$ について $(-) \times A$ が右随伴 $(-)^{A}$ を持つとき、 $C$ はcartesian closed categoryと呼ばれる。

ロジックに慣れている人向けの定義

cartesian closed categoryとは10個組 $(C, T, \land, \supset, o, p, q, e, ⟨ ⟩,^{*})$ であって、以下の条件を満たすものを言う。

$C$ はcategory。
$T$ は $C$ のobject。
$\land, \supset$ はそれぞれ、 $C$ のobjectの組 $(A, B)$ を受け取ってobject $A \land B$ , $A \supset B$ を与える演算。
$o$ は $C$ のobject $A$ を受け取って射 $o_{A} : A \to T$ を与える割り当て。
$p, q, e$ はそれぞれ、 $C$ のobjectの組 $(A, B)$ を受け取って射 $p_{A, B} : A \land B \to A, q_{A, B} : A \land B \to B, e_{A, B} : (B \supset A) \land B \to A$ を与える割り当て。
$⟨ ⟩$ は $C$ のdomainを同じくする射の組 $(f : A \to C, g : A \to D)$ を受け取って、射 $⟨ f, g ⟩ : A \to C \land D$ を与える演算。
$^{*}$ は $C$ の射 $f : C \times B \to A$ を受け取って、射 $f^{*} : C \to B \supset A$ を与える演算。
以下の等式が成立する。
1. $f = o_{A}$ for any $f : A \to T$
2. $p_{A, B} ⟨ f, g ⟩ = f$
3. $q_{A, B} ⟨ f, g ⟩ = g$
4. $⟨ p_{A, B} h, q_{A, B} h ⟩ = h$
5. $e_{A, B} ⟨ f^{*} p_{C, B}, q_{C, B} ⟩ = f$
6. $(e_{A, B} ⟨ h p_{C, B}, q_{C, B} ⟩)^{*} = h$