デカルト閉圏
圏論において、圏がデカルト閉（デカルトへい、英語: cartesian closed）であるとは、大雑把に言えば任意の二つの対象の直積上で定義される射が直積因子の一方で定義される射と自然に同一視できることである。デカルト閉な圏はラムダ計算の自然な設定ができるという点で数理論理学およびプログラミングの理論において特に重要である。デカルト閉圏の概念はモノイド圏に一般化される（モノイド閉圏を参照）。
定義
[編集]圏 C がデカルト閉であるとは、以下の三条件
が全て満たされることをいう。上ふたつの条件は、組み合わせて「C の対象からなる任意の有限族（空でも構わない）に対し、それらの直積対象が C に存在する」という一つの条件に読み替えることができる。これは、圏における直積が自然な結合性をもつことと、圏における空積はその圏の終対象となることとに拠る。
3番目の条件は圏 C の任意の対象 Y に対して、関手 – × Y（すなわち、C から C への関手であって、任意の対象 X に対し X × Y を対応させ、任意の射 φ に対し φ × idY を対応させるもの）が右随伴 –Y を持つこと仮定することに同値である。これはまた、hom-集合の間に双射
で X と Z の両方に関して自然変換となっているものが存在することとも言い換えられる。
任意のスライス圏がデカルト閉であるような圏は、局所デカルト閉 (locally cartesian closed) であるという。
例
[編集]デカルト閉圏の例として以下のようなものが挙げられる。
- 集合全体が写像を射として成す、集合の圏 Set はデカルト閉である。この圏における直積 X × Y は X と Y との直積集合、冪対象 ZY は Y から Z への写像全体の成す配置集合である。随伴性は以下の事実写像 f: X × Y → Z はそれが誘導する写像 g : X → ZY (g(x)(y) = f(x,y) for all x ∈ X, y ∈ Y) と自然に同一視できる。によって表される。
- 有限集合が写像を射として成す、有限集合の圏も同じ理由でデカルト閉である。
- G を群とするとき、G-集合全体の成す圏もデカルト閉である。Y, Z をふたつの G-集合とするとき、冪対象 ZY は Y から G への配置集合に G の作用を (g.F)(y) = g.(F(g−1.y)) (g ∈ G, F: Y → Z, y ∈ Y) によって定めたものである。
- 有限 G-集合の圏もやはりデカルト閉圏になる。
- 小さい圏が関手を射として成す、圏の圏 Cat もデカルト閉圏である。冪対象 CD は D から C への関手全体が自然変換を射として成す関手圏で与えられる。
- C が小さい圏ならば、C から集合の圏への共変関手が自然変換を射として成す関手圏 SetC はデカルト閉である。F, G を C から Set への関手とすると、冪対象 FG は、C の任意の対象 X に対して (X, –)× G から F への自然変換全体の成す集合を対応させる関手で与えられる。
- 上で述べた G-集合の圏の例は関手圏の特別の場合と見ることができる。実際、任意の群を唯一つの対象を持つ圏と見なせば、G-集合はこの圏から集合の圏 Set への関手に他ならない。
- 有向グラフの圏も関手圏であるから、デカルト閉圏である。
- 代数的位相幾何学において、デカルト閉圏の連帯は特に簡単である。位相空間全体が連続写像に関して成す圏も可微分多様体が滑らかな写像に関して成す圏もデカルト閉圏とはならない。代わりとなる圏は既に考えられていて、コンパクト生成ハウスドルフ空間の圏はデカルト閉である。また、Frölicher空間の圏も同様である。
- 順序集合論において、完備半順序集合 (cpo) は自然な位相としてスコット位相を持ち、その連続写像の全体がデカルト閉圏を成す（すなわち、その対象は cpo それ自体のみであり、スコット連続写像を射とするような圏を考える）。カリー化と「適用」はともにスコット位相に関して連続であり、カリー化は適用を伴って随伴を導く[1]。
- ハイティング代数はデカルト閉な半順序集合である。位相空間から重要な例が生じる。X を位相空間とすると、X の開集合の全体を対象とする圏 O(X) が考えられる。その対象 U から V への射は、U が V の部分集合であるときただ一つのみ存在し、そうでないときには存在しないものとして定められる。この包含関係による半順序集合はデカルト閉であり、この圏における U と V との直積は U と V との共通部分によって与えられ、冪対象 UV は U ∪(X\V) の開核である。
デカルト閉ではない圏の例には以下のようなものが挙げられる。
- 固定された体上のベクトル空間全体の成す圏や有限次元ベクトル空間の圏はともにデカルト閉ではない。これらの圏は「直和」と呼ばれる直積は持つけれども、直積関手の右随伴が存在しない（これらの圏は対称モノイド閉圏ではある。ベクトル空間の間の線型写像全体の成す集合は再びベクトル空間をなすという意味で閉であり、直積の代わりにテンソル積を考えれば Hom-集合の間に同様の同型が存在する）。
- アーベル群の圏も同様の理由でデカルト閉ではない。
応用
[編集]デカルト閉圏において、「二変数関数」（つまり、射 f: X × Y → Z）は常に「一変数関数」（つまり射 λf: X → ZY）として表現できる。計算機科学における応用ではこれはカリー化として知られ、単純型付ラムダ計算の任意のデカルト閉圏における解釈を実現に導く。
カリー-ホワード-ランベック対応は直観主義論理、単純型付ラムダ計算、デカルト閉圏の間の深い同型を与える。
トポスという種類のデカルト閉圏は、数学に対する従来の集合論に替わる一般的な枠組みとして提示された。
高名な計算幾何学者ジョン・バッカスは（後から考えるとデカルト閉圏の内部言語にどこか似たところのある）無変数記法あるいは関数レベルプログラミングを提唱した。CAMLはデカルト閉圏のさらに意識的なモデルである。
方程式論
[編集]任意のデカルト閉圏において（冪記法を用いて）、(XY)Z と (XZ)Y は任意の対象 X, Y, Z に対して同型である。これを等式の形で
- (xy)z = (xz)y.
と書き表す。任意のデカルト閉圏において、ほかに有効な等式にはどんなものがあるだろうか。これについては、以下の公理に従って論理的にすべての有効な等式を計算することができる[2]。
- x ×(y × z) = (x × y)× z
- x × y = y × x
- x × 1 = x （1 は C の終対象）
- 1x = 1
- x1 = x
- (x×y)z = xz × yz
- (xy)z = x(y × z)
脚注
[編集]- ^ H.P. Barendregt, The Lambda Calculus, (1984) North-Holland ISBN 0-444-87508-5 (See theorem 1.2.16)
- ^ S. Soloviev. "Category of Finite Sets and Cartesian Closed Categories", Journal of Soviet Mathematics, 22, 3 (1983)
参考文献
[編集]- F. William Lawvere (1963), Functorial Semantics of Algebraic Theories
- F. William Lawvere (2004), Functorial Semantics of Algebraic Theories and Some Algebraic Problems in the context of Functorial Semantics of Algebraic Theories
- F. William Lawvere (1964), An Elementary Theory of the Category of Sets
- F. William Lawvere (2005), An elementary theory of the category of sets (long version) with commentary
- F. William Lawvere (2006), Adjointness in foundations, with author commentary
- J. Lambek, P.J. Scott (1988). Introduction to Higher-Order Categorical Logic
- 疋田 輝雄 (1991), カテゴリー理論とプログラミング : カルテシアン閉カテゴリー
- 井田 哲雄 (1987), ラムダ計算とそのモデル「カルテシアン閉カテゴリ」によるCOMMON LISPの解釈と新しい処理系
史学的観点からのもの
[編集]- A.F. Monna 著、鶴見 和之 , 新井 理生 (訳) 編『現代数学発展史―現代数学の進展 方法・概念・思想の変遷』東京電機大学出版局、1993年。 p.61-63
