デカルトの閉カテゴリ

圏論では、大まかに言えば、2つのオブジェクトの積に定義された任意の射が、いずれかの因子に定義された射と自然に同一視できる場合、圏はカルティシアン閉である。これらの圏は、その内部言語が単純型付きラムダ計算であるため、数理論理学やプログラミング理論において特に重要である。これらは、内部言語である線形型システムが量子計算と古典計算の両方に適している閉じたモノイド圏によって一般化される。 ^[1]

フランスの哲学者、数学者、科学者であるルネ・デカルト（1596年 - 1650年）にちなんで名付けられました。デカルトの解析幾何学の定式化により、デカルト積の概念が生まれ、これが後に圏積の概念に一般化されました。

カテゴリCは、次の3つの性質を満たす 場合にのみ、カルティシアン閉^{[2]と呼ばれます。}

• 終端オブジェクトがあります。
• Cの任意の 2 つのオブジェクトXとYには、 C内で積X  × Yが存在します。
• Cの任意の 2 つのオブジェクトYとZには、 C内で指数Z ^{Y が}存在します。

最初の 2 つの条件は、カテゴリ積の自然な結合性と、カテゴリ内の空積がそのカテゴリの終端オブジェクトであるため、 Cの任意の有限 (空である可能性もある) オブジェクトのファミリがC内の積を許容するという単一の要件に組み合わせることができます。

3番目の条件は、関数– × Y （つまり、 CからCへの関数で、対象XをX  × Yに、射 φ を φ × id _Yに写すもの）が、 C内のすべての対象Yに対して、通常 – ^Yと表記される右随伴関数を持つという要件と同等である。局所的に小さいカテゴリの場合、これはホム集合間の一対一の存在によって表現できる。

${\displaystyle \mathrm {Hom} (X\times Y,Z)\cong \mathrm {Hom} (X,Z^{Y})}$

これはX、Y、Zにおいて自然である。^[3]

デカルトの閉カテゴリには有限の限界がある必要はなく、有限の積のみが保証されることに注意してください。

あるカテゴリがそのすべてのスライスカテゴリが直交閉であるという性質を持つ場合、そのカテゴリは局所直交閉と呼ばれる。^[4] Cが局所直交閉である場合、それが実際に直交閉である必要はないことに注意する。直交閉は、 Cが終端オブジェクトを持つ 場合にのみ発生する。

各オブジェクトYに対して、指数的随伴の余単位は自然変換である。

${\displaystyle \mathrm {ev} _{Y,Z}:Z^{Y}\times Y\to Z}$

これを（内部）評価マップと呼ぶ。より一般的には、部分適用マップを複合マップとして 構築することができる。

${\displaystyle \mathrm {papply} _{X,Y,Z}:Z^{X\times Y}\times X\cong (Z^{Y})^{X}\times X{\xrightarrow {\mathrm {ev} _{X,Z^{Y}}}}Z^{Y}.}$

カテゴリSetの特定のケースでは、これらは通常の操作に簡約されます。

${\displaystyle \mathrm {ev} _{Y,Z}(f,y)=f(y).}$

射p  : X → Yにおいて指数関数を1つの引数で評価すると、射が得られる。

${\displaystyle p^{Z}:X^{Z}\to Y^{Z},}$

${\displaystyle Z^{p}:Z^{Y}\to Z^{X},}$

pとの合成演算に対応します。演算p ^{Z の}代替表記にはp _*やp∘- などがあります。演算Z ^pの代替表記にはp ^*や-∘pなどがあります。

評価マップは次のように連鎖できる。

${\displaystyle Z^{Y}\times Y^{X}\times X{\xrightarrow {\mathrm {id} \times \mathrm {ev} _{X,Y}}}Z^{Y}\times Y{\xrightarrow {\mathrm {ev} _{Y,Z}}}Z}$

指数的付加の下の対応する矢印

${\displaystyle c_{X,Y,Z}:Z^{Y}\times Y^{X}\to Z^{X}}$

（内部）構成マップと呼ばれます。

カテゴリSetの特定のケースでは、これは通常の合成操作です。

${\displaystyle c_{X,Y,Z}(g,f)=g\circ f.}$

射p : X → Yに対して、 pとの合成が恒等写像となる写像に対応するX ^Yの部分オブジェクトを定義する次のプルバック スクエアが存在するものとします。

${\displaystyle {\begin{array}{ccc}\Gamma _{Y}(p)&\to &X^{Y}\\\downarrow &&\downarrow \\1&\to &Y^{Y}\end{array}}}$

ここで、右側の矢印はp ^Yであり、下の矢印はY上の恒等式に対応します。Γ _Y ( p ) はpの切断の対象と呼ばれます。これはしばしば Γ _Y ( X )と略されます。

_{Γ Y} ( p ) がY を余域とするすべての射pに対して存在する場合、それはスライスカテゴリ上の関手 Γ _Y  : C / Y → Cに組み立てることができ、これは積関手の変種に右随伴する:

${\displaystyle \hom _{C/Y}(X\times Y{\xrightarrow {\pi _{2}}}Y,Z{\xrightarrow {p}}Y)\cong \hom _{C}(X,\Gamma _{Y}(p)).}$

Yの指数はセクションで表現できます。

${\displaystyle Z^{Y}\cong \Gamma _{Y}(Z\times Y{\xrightarrow {\pi _{2}}}Y).}$

デカルトの閉カテゴリの例には次のものがあります。

• 関数を射として持つすべての集合のカテゴリSetは、直積閉です。積X × YはXとYの直積であり、Z ^{Y は}YからZへのすべての関数の集合です。随伴性は次の事実によって表現されます。関数f  : X × Y → Zは、すべての x が X に、 yがYにそれぞれ存在する場合、g ( x )( y ) = f ( x , y )で定義されるカリー化関数g  : X → Z ^Yと自然に同一視されます。
• 関数を射として持つ有限集合のカテゴリは、同じ理由でデカルト的に閉じています。
• Gが群である場合、すべてのG集合のカテゴリは直交閉です。YとZ が2 つのG集合である場合、Z ^{Y は}、すべての g がGに含まれ、 F : Y → Zであり、 yがYに含まれる場合、 Gの作用は( g . F )( y ) = g . F ( g ⁻¹ . y)で定義される、 YからZへのすべての関数の集合です。
• 有限G集合のカテゴリもデカルト的に閉じています。
• すべての小さなカテゴリ（関数を射として持つ）のカテゴリCatは、デカルト閉です。指数関数C ^{D は、}自然変換を射として持つ、DからCまでのすべての関数からなる関数カテゴリによって与えられます。
• C が小さなカテゴリである場合、Cから集合のカテゴリへの共変関手すべてと、射としての自然変換から構成される関手カテゴリSet ^{C は}、直積閉です。 FとGがCからSetへの2つの関手である場合、指数関数F ^Gは、 CのオブジェクトX上の値が( X ,−) ×  GからFへのすべての自然変換の集合によって与えられる関手です。
  • 前述のG集合の例は、関数カテゴリの特別なケースとして見ることができます。すべてのグループは1つのオブジェクトのカテゴリと見なすことができ、G集合はこのカテゴリからSetへの関数に他なりません。
  • すべての有向グラフのカテゴリは直交閉です。これは、関数カテゴリで説明されている関数カテゴリです。
  • 特に、単体集合（関数X  : Δ ^op → Set）のカテゴリはデカルト閉です。
• さらに一般的に言えば、すべての基本トポスはデカルト的に閉じています。
• 代数的位相幾何学では、直交閉圏は特に扱いやすい。連続写像を持つ位相空間の圏も滑らかな写像を持つ滑らかな多様体の圏も直交閉圏ではない。そのため、代わりの圏が検討されている。コンパクトに生成されたハウスドルフ空間の圏は直交閉圏であり、フレーリッヒャー空間の圏も同様である。
• 順序論では、完全半順序（cpo）は自然な位相、スコット位相を持ち、その連続写像はデカルトの閉カテゴリを形成します（つまり、オブジェクトはcpoであり、射はスコット連続写像です）。カリー化と適用はどちらもスコット位相の連続関数であり、カリー化は適用とともに随伴関数を提供します。^[5]
• ヘイティング代数は、直交閉（有界）格子です。重要な例は位相空間から生じます。Xが位相空間である場合、Xの開集合はカテゴリ O( X ) の対象を形成します。このカテゴリには、 U がVのサブセットである場合にUからVへの一意の射があり、そうでない場合は射がありません。このposet は直交閉カテゴリです。UとVの「積」はUとVの共通部分であり、指数U ^{V は}U ∪( X \ V )の内部です。
• ゼロオブジェクトを持つカテゴリがカルティシアン閉であるのは、それが1つのオブジェクトと1つの恒等射だけを持つカテゴリと同値である場合に限ります。実際、0が初期オブジェクトで1が最終オブジェクトであり、 である場合、は1つの要素のみを持ちます。^[6]${\displaystyle 0\cong 1}$${\displaystyle \mathrm {Hom} (X,Y)\cong \mathrm {Hom} (1,Y^{X})\cong \mathrm {Hom} (0,Y^{X})\cong 1}$
  • 特に、アーベル圏などの零対象を持つ非自明な圏は、デカルト閉ではありません。したがって、環上の加群の圏はデカルト閉ではありません。ただし、固定された加群を持つ関数テンソル積には 右随伴があります。テンソル積は圏積ではないため、これは上記と矛盾しません。代わりに、加群の圏はモノイド閉 であることがわかります。${\displaystyle -\otimes M}$

局所的にデカルト的に閉じたカテゴリの例には次のものがあります。

• すべての基本トポスは局所的に直交閉路です。この例には、グループGのSet、FinSet、G集合、および小さなカテゴリCのSet ^Cが含まれます。
• 対象が位相空間で射が局所同相であるカテゴリLH は、 LH/X が層のカテゴリ⁠ ⁠と同値であるため、局所的にデカルト閉です。ただし、LH には終端対象がないため、デカルト閉ではありません。${\displaystyle Sh(X)}$
• C にプルバックがあり、すべての矢印p  : X → Yに対して、プルバックを取ることによって与えられる関数p ^*  : C/Y → C/Xに右随伴関数がある場合、C は局所的にデカルト閉です。
• Cが局所的に直交閉である場合、そのスライス カテゴリC/Xもすべて局所的に直交閉です。

局所的にデカルト的に閉じたカテゴリの非例には次のものがあります。

• Cat は局所的にデカルト的に閉じていません。

デカルト閉圏では、「2 変数の関数」（射f  : X × Y → Z）は常に「1 変数の関数」（射 λ f  : X → Z ^Y）として表すことができます。コンピュータ サイエンスのアプリケーションでは、これはカリー化として知られています。これにより、単純に型付けされたラムダ計算は、任意のデカルト閉圏で解釈できるという認識が生まれました。

カリー・ハワード・ランベック対応は、直観主義論理、単純型ラムダ計算、およびデカルトの閉カテゴリ間の深い同型性を提供します。

伝統的な集合論の代わりに、数学の一般的な設定として、特定のデカルトの閉カテゴリであるトポイが提案されています。

コンピュータ科学者のジョン・バッカスは、変数を使わない表記法、つまり関数レベルプログラミングを提唱しているが、これは振り返ってみると、デカルト閉圏の内部言語とある程度類似している。 ^[7] CAMLは、より意識的にデカルト閉圏をモデルにしている。

C を局所的にデカルト閉カテゴリとします。すると、共領域Zを持つ 2 つの矢印のプルバックはC/Zの積で与えられるため、 C にはすべてのプルバックが存在します。

すべての矢印p  : X → Yについて、P がC/Yの対応するオブジェクトを表すものとします。 pに沿って引き戻すと、左と右の両方の随伴関数を持つ関数p ^*  : C/Y → C/Xが得られます。

左随伴は従属和と呼ばれ、合成によって与えられます。 ${\displaystyle \Sigma _{p}:C/X\to C/Y}$${\displaystyle p\circ (-)}$

右の随伴関数は従属積と呼ばれます。 ${\displaystyle \Pi _{p}:C/X\to C/Y}$

C/YにおけるPの指数は、従属積を用いて式 で表すことができます。 ${\displaystyle Q^{P}\cong \Pi _{p}(p^{*}(Q))}$

これらの名前の理由は、P を依存型 として解釈する場合、関数とがそれぞれ型構成とに対応するためです。 ${\displaystyle y:Y\vdash P(y):\mathrm {Type} }$${\displaystyle \Sigma _{p}}$${\displaystyle \Pi _{p}}$${\displaystyle \Sigma _{x:P(y)}}$${\displaystyle \Pi _{x:P(y)}}$

あらゆるデカルトの閉圏（指数表記法を使用）において、（X ^Y）^Zと（X ^Z）^YはすべてのオブジェクトX、Y、Zに対して同型である。これを「方程式」と書く。

（xy）^{z =}（xz）^y。^​

他にどのような方程式がすべてのデカルト閉圏で有効であるかを尋ねる人もいるかもしれない。それらはすべて、次の公理から論理的に導かれることが判明している。^[8]

• x × ( y × z ) = ( x × y ) × z
• x × y = y × x
• x ×1 = x （ここで 1 はCの終端オブジェクトを表します）
• 1 ^× =1
• x ¹ = x
• ( x × y ) ^z = x ^z × y ^z
• ( x ^y ) ^z = x ^{( y × z )}

双カルティジアン閉圏は、積が余積上に分配される、二項余積と初期オブジェクトを持つカルティジアン閉圏を拡張します。それらの等式理論は次の公理で拡張され、ゼロを含む タルスキの高校の公理に似たものになります。

• x + y = y + x
• ( x + y ) + z = x + ( y + z )
• x × ( y + z ) = x × y + x × z
• x ^{( y + z )} = x ^y ×x ^z
• 0 + x = x
• × 0 = 0
• x ⁰ = 1

ただし、上記のリストは完全ではないことに注意してください。自由BCCCの型同型性は有限に公理化できず、その決定可能性は未解決の問題です。^[9]

• nラボのデカルト閉カテゴリ
• Baez, John (2006)。「CCC と λ 計算」。n-Category Café: 数学、物理学、哲学に関するグループ ブログ。テキサス大学。