デカルト圏の等式的定義 細かいこと色々
そういう事情で、デカルト圏の定義に関する細かいことまでメモするぞ、っと。
圏論の極限の立場では、「デカルト性＝離散有限完備＝離散有限図式の極限が常に存在」となる。一方で、コラディニ／ガダッチ／セリンガー（Corradini/Gaddacci/Selinger）は対角（余積、余乗法、余和）Δによる余モノイドを基本にしている。それらの中間にランベック／スコット（Lambek/Scott）のペアリング<-, ->を使う流儀がある。
注意すべきは、離散有限完備では、極限（i.e. 有限直積）はup-to-isoでしか決まらない。それに対して等式的な（対角でもペアリングでも）定義では、特定された（distinguished, selected）終対象1と、特定された二項演算／余二項演算（ペアリング／対角）が確定的に与えられている点だ。
よって、等式的なデカルト圏と直接的に対応するのは、特定された極限を持つ離散有限完備圏である。つまり、Cの離散図式Dに対して、Lim(D)∈Cone(C, D)が一意的に定まる。Cone(C, D)は、圏C内の底面がDである錐の圏。数学的帰納法を使えば、Lim(2)（2 = {1, 2}）の存在から、Lim(n)（n≧2）の存在を言えるから、二項直積が本質ではある。つまり、次が同値：
- 任意の離散有限図式Dに対してLim(D)が確定する。
- Lim(0)とLim(2)が確定する。（0は空集合）
- 終対象を特定でき、二項直積も特定できる。
さらに、「二項直積も特定できる」を言い換えると：
- 対象に対する二項直積対象と、対応する射影対（π、π'）を特定できる。
結局、対象の対A, Bで添字付けられた直積システム (PA,B, πA,B, π'A,B)が特定できればいい。このスパンが、直積としての普遍性を持つために、ペアリング<-, ->X,A,B : Hom(X, A)×Hom(X, B) → Hom(X, A×B) も備える必要がある。これがランベック／スコット流の定義。
ランベック／スコット流の等式的定義は、「Lim(0)とLim(2)が確定している圏」の直接的なパラフレーズだから、相当に（心理的な）自然感がある。一方、コラディニ／ガダッチ／セリンガー流の、余モノイドから入るスタイルは、デカルト性が明白でなくて分かりにくい（僕は分からなかった）。しかし、コピー可能f;Δ = Δ;(f×f)、破棄可能 f;! = ! などの概念は使い勝手がよい。セリンガーが注意してるように、多値写像（関係）の圏では、コピー可能は単葉（univalent）であり、破棄可能は全域（total、exact）である。多値写像の圏の焦点圏は、集合と普通の写像の圏である。
