デカルト閉圏
圏論の世界には様々な構造を持つ圏が存在しますが、その中でも「デカルト閉圏（Cartesian Closed Category）」は、数理論理学や計算機科学の理論、特にラムダ計算と密接に関わる重要な概念です。
デカルト閉圏とは、対象間の直積と、特定の性質を持つ「冪対象」が存在し、両者の間で自然な対応関係が成り立つ圏を指します。より直感的に言えば、複数の入力を取る関数を、最初の入力だけを取り残りの入力を取る関数を返すような、単一の入力を取る関数と同一視できる性質（これは計算機科学におけるカリー化に相当します）が、圏の構造として定式化されたものです。これは、モノイド閉圏と呼ばれる、より一般的な概念の特定のケースとして位置づけられます。
圏Cがデカルト閉であるためには、以下の3つの条件を全て満たす必要があります。
1. 終対象の存在: 圏Cには、任意の対象からただ一つの射が存在する「終対象」と呼ばれる特別な対象が存在する。
2. 直積の存在: 圏Cの任意の2つの対象XとYに対して、それらの「直積」X × Y が存在する。これは、圏における直積の結合性や、空な対象族の直積が終対象となる性質から、圏Cの対象からなる任意の有限族（空の場合も含む）に対して、それらの直積対象が存在することと同等です。
3. 冪対象の存在: 圏Cの任意の2つの対象YとZに対して、YからZへの射全体を「対象」として持つと見なせるような「冪対象」Z^Yが存在する。
特に3番目の条件は、圏論的な随伴性によって言い換えることができます。すなわち、圏Cの任意の対象Yに対して、対象XをX×Yへ写す関手（これはXからX×Yへの射を、φ: X→X'に対してφ×id_Y: X×Y→X'×Yへ写す関手）が、対象XをZ^Yへ写す関手に対して右随伴関手を持つことと同値です。これはまた、圏Cの任意の対象X, Y, Zに対し、Hom(X×Y, Z)（X×YからZへの射の集合）とHom(X, Z^Y)（XからZ^Yへの射の集合）の間に、XとZに関して自然な全単射が存在することとしても定式化されます。
圏Cの任意のスライス圏（特定の対象を基点とする、その対象への射とそれらの可換図式で構成される圏）がデカルト閉であるとき、その圏Cは「局所デカルト閉」であると言われます。
デカルト閉圏は様々な数学や計算機科学の分野に現れます。代表的な例としては以下のようなものがあります。
集合の圏 (Set): 対象は集合、射は写像。直積は集合の直積、冪対象は写像全体の集合です。
有限集合の圏: 有限集合と写像の圏。Setと同様の理由でデカルト閉です。
G-集合の圏: 群Gが作用する集合とG同変写像の圏。冪対象には適切なGの作用が定義されます。
小さな圏の圏 (Cat): 対象は小さな圏、射は関手。冪対象は関手圏（射は自然変換）です。
関手圏 Set^C: 小さな圏Cから集合の圏Setへの共変関手と自然変換の圏。
コンパクト生成ハウスドルフ空間の圏やFrölicher空間の圏: 位相空間全体や可微分多様体の圏はデカルト閉ではありませんが、これらの圏はデカルト閉となります。
完備半順序集合 (cpo) の圏: スコット連続写像を射とするcpoの圏。カリー化と適用が連続写像となります。
ハイティング代数: 論理学と関連が深く、半順序集合として見た場合にデカルト閉です。特に、位相空間Xの開集合全体が包含関係でなす順序集合O(X)もデカルト閉圏となり、直積は共通部分、冪対象は開核で定義されます。
* ベクトル空間の圏やアーベル群の圏: これらの圏は直積（直和）を持ちますが、直積関手に対する右随伴が存在しないため、デカルト閉ではありません。ただし、これらはテンソル積を考えることでモノイド閉圏にはなります。
デカルト閉圏の最も強力な応用の一つは、計算機科学における「カリー化」の概念を圏論的に捉えられることです。対象X×YからZへの射（二変数関数に相当）が、対象Xから冪対象Z^Yへの射（カリー化された一変数関数に相当）と自然な同型を通じて結びつけられます。この性質は、単純型付ラムダ計算を任意のデカルト閉圏の中で意味論的に解釈する際の基礎となります。
さらに、圏論、数理論理学（特に直観主義論理）、型付ラムダ計算の間には「カリー-ハワード-ランベック対応」と呼ばれる深い構造的な対応があり、デカルト閉圏はこの対応の中心的な概念となっています。集合論の代替となる基礎理論として提案された「トポス」も、特定の種類のデカルト閉圏です。
計算機科学者ジョン・バッカスが提唱した関数レベルプログラミングや、関数型プログラミング言語CAMLなども、デカルト閉圏の考え方と関連が見られます。
任意のデカルト閉圏において、冪記法を用いて書くと、対象(X^Y)^Zは(X^Z)^Yと同型になります。これは(x^y)^z = (x^z)^yという等式の形で表現される性質です。デカルト閉圏で成り立つすべての等式は、直積の結合性、可換性、終対象との関係、そして冪対象に関する特定の公理から論理的に導き出すことができます。
デカルト閉圏は、直積と冪対象という基本的な圏論的構造を通じて、カリー化のような普遍的な計算の概念や論理構造を捉える枠組みを提供します。その豊かな性質は、理論計算機科学、数理論理学、プログラミング言語理論など、様々な分野で基礎的な役割を果たしています。
デカルト閉圏とは
デカルト閉圏とは、対象間の直積と、特定の性質を持つ「冪対象」が存在し、両者の間で自然な対応関係が成り立つ圏を指します。より直感的に言えば、複数の入力を取る関数を、最初の入力だけを取り残りの入力を取る関数を返すような、単一の入力を取る関数と同一視できる性質（これは計算機科学におけるカリー化に相当します）が、圏の構造として定式化されたものです。これは、モノイド閉圏と呼ばれる、より一般的な概念の特定のケースとして位置づけられます。
厳密な定義
圏Cがデカルト閉であるためには、以下の3つの条件を全て満たす必要があります。
1. 終対象の存在: 圏Cには、任意の対象からただ一つの射が存在する「終対象」と呼ばれる特別な対象が存在する。
2. 直積の存在: 圏Cの任意の2つの対象XとYに対して、それらの「直積」X × Y が存在する。これは、圏における直積の結合性や、空な対象族の直積が終対象となる性質から、圏Cの対象からなる任意の有限族（空の場合も含む）に対して、それらの直積対象が存在することと同等です。
3. 冪対象の存在: 圏Cの任意の2つの対象YとZに対して、YからZへの射全体を「対象」として持つと見なせるような「冪対象」Z^Yが存在する。
特に3番目の条件は、圏論的な随伴性によって言い換えることができます。すなわち、圏Cの任意の対象Yに対して、対象XをX×Yへ写す関手（これはXからX×Yへの射を、φ: X→X'に対してφ×id_Y: X×Y→X'×Yへ写す関手）が、対象XをZ^Yへ写す関手に対して右随伴関手を持つことと同値です。これはまた、圏Cの任意の対象X, Y, Zに対し、Hom(X×Y, Z)（X×YからZへの射の集合）とHom(X, Z^Y)（XからZ^Yへの射の集合）の間に、XとZに関して自然な全単射が存在することとしても定式化されます。
局所デカルト閉圏
圏Cの任意のスライス圏（特定の対象を基点とする、その対象への射とそれらの可換図式で構成される圏）がデカルト閉であるとき、その圏Cは「局所デカルト閉」であると言われます。
デカルト閉圏の例
デカルト閉圏は様々な数学や計算機科学の分野に現れます。代表的な例としては以下のようなものがあります。
集合の圏 (Set): 対象は集合、射は写像。直積は集合の直積、冪対象は写像全体の集合です。
有限集合の圏: 有限集合と写像の圏。Setと同様の理由でデカルト閉です。
G-集合の圏: 群Gが作用する集合とG同変写像の圏。冪対象には適切なGの作用が定義されます。
小さな圏の圏 (Cat): 対象は小さな圏、射は関手。冪対象は関手圏（射は自然変換）です。
関手圏 Set^C: 小さな圏Cから集合の圏Setへの共変関手と自然変換の圏。
コンパクト生成ハウスドルフ空間の圏やFrölicher空間の圏: 位相空間全体や可微分多様体の圏はデカルト閉ではありませんが、これらの圏はデカルト閉となります。
完備半順序集合 (cpo) の圏: スコット連続写像を射とするcpoの圏。カリー化と適用が連続写像となります。
ハイティング代数: 論理学と関連が深く、半順序集合として見た場合にデカルト閉です。特に、位相空間Xの開集合全体が包含関係でなす順序集合O(X)もデカルト閉圏となり、直積は共通部分、冪対象は開核で定義されます。
デカルト閉ではない例
* ベクトル空間の圏やアーベル群の圏: これらの圏は直積（直和）を持ちますが、直積関手に対する右随伴が存在しないため、デカルト閉ではありません。ただし、これらはテンソル積を考えることでモノイド閉圏にはなります。
応用と重要性
デカルト閉圏の最も強力な応用の一つは、計算機科学における「カリー化」の概念を圏論的に捉えられることです。対象X×YからZへの射（二変数関数に相当）が、対象Xから冪対象Z^Yへの射（カリー化された一変数関数に相当）と自然な同型を通じて結びつけられます。この性質は、単純型付ラムダ計算を任意のデカルト閉圏の中で意味論的に解釈する際の基礎となります。
さらに、圏論、数理論理学（特に直観主義論理）、型付ラムダ計算の間には「カリー-ハワード-ランベック対応」と呼ばれる深い構造的な対応があり、デカルト閉圏はこの対応の中心的な概念となっています。集合論の代替となる基礎理論として提案された「トポス」も、特定の種類のデカルト閉圏です。
計算機科学者ジョン・バッカスが提唱した関数レベルプログラミングや、関数型プログラミング言語CAMLなども、デカルト閉圏の考え方と関連が見られます。
方程式論
任意のデカルト閉圏において、冪記法を用いて書くと、対象(X^Y)^Zは(X^Z)^Yと同型になります。これは(x^y)^z = (x^z)^yという等式の形で表現される性質です。デカルト閉圏で成り立つすべての等式は、直積の結合性、可換性、終対象との関係、そして冪対象に関する特定の公理から論理的に導き出すことができます。
まとめ
デカルト閉圏は、直積と冪対象という基本的な圏論的構造を通じて、カリー化のような普遍的な計算の概念や論理構造を捉える枠組みを提供します。その豊かな性質は、理論計算機科学、数理論理学、プログラミング言語理論など、様々な分野で基礎的な役割を果たしています。
もう一度検索
【記事の利用について】
タイトルと記事文章は、記事のあるページにリンクを張っていただければ、無料で利用できます。
※画像は、利用できませんのでご注意ください。
【リンクついて】
リンクフリーです。