2005-02-15 [長年日記]
λ. 不動点と有限直和を持つCCC
A Model of Intuitionistic Affine Logic from Stable Domain Theory, Torben Braüner によれば、A Note on Inconsistencies caused by Fixpoints in a Cartesian Closed Category. Huwig, Hagen, Poigné で、「不動点と有限直和を持つCCC(Cartesian Closed Category)は、一つの対象と一つの射しかない圏と圏同値」(a cartesian closed category with fixpoints and finite sums is equivalent to the category with one object and one arrow.
)が示されているそうだ。この論文はWeb上には公開されてないみたいだし、メディアセンターで取り寄せるのも面倒なので、その前にちょっと考えてみる。
まず、A Model of Intuitionistic Affine Logic from Stable Domain Theoryから不動点の定義を引っ張ってきておこう。
- 不動点
-
有限直積を持つ圏は、 任意の射 f: A×B→B について 射 f†: A→B が存在して f† = f o (idA×f†) o ΔA (ここで ΔA: A → A×A は対角化写像 ΔA = <idA,idA>) を満たすときに、「不動点を持つ」と言う。 また、この f†: A→B を f: A×B→B の不動点と呼ぶ。
なお、CCCが不動点を持つのは、 任意の対象Bに対して不動点演算子 YB: BB → B が存在して、 任意のf: A×B→B について YB o curry(f) が f の不動点に なっている時かつその時だけだそうだ。
有限個の対象の直和が存在すると言っているので、ゼロ個の対象の直和、すなわち始対象0も存在する*1。そして、p2: 1×0→0 の不動点 p2†: 1→0 は !0: 0→1 の逆射になっているので 0 ≅ 1。 一方、uncurry(!!0A): 0×A→0 は !!0×A: 0→0×A の逆射になっているので、 0×A ≅ 0。 したがって、任意のAについて A ≅ 1×A ≅ 0×A ≅ 0 なので、全ての対象は同型。
次に、任意の対象X,Yを考える。Xから0への同型射をα: X→0、1からYへの同型射をβ: 1→Y とすると、任意の射 f: X→Y について β-1 o f o α-1 = !0 が成り立ち f = β o !0 o α であるので、射 X→Y はただ一つだけしか存在しない。
ここまでで、この圏は全ての対象が同型で、どの対象X,Yの間にも射は一つだけしか存在しないような、つまらない圏でしかないことが分かった。ちなみに、ここまでは “Conceptual Mathematics: A First Introduction to Categories”, F. William Lawvere, Stephen H. Schanuel の知識だけから言えるはず。最後に、この圏が一つの対象と一つの射しかない圏と圏同値であることは……省略。
……と、ここまで書いてきてなんなんだが、なんか変な気がするなぁ……
*1 有限つったら普通ゼロも含んでるよね?
λ. 不動点と有限直和を持つCCC (2)
具体例として、全ての pointed CPO と全ての正格な連続関数からなる圏を考えてみる。この圏では 0 = 1 = {⊥} となっていて直積も存在する。もし、冪(exponential)が存在してCCCになっているなら、さっきの議論からこの圏の全ての対象は同型だということになるけど、これは矛盾。したがって、この圏には冪は存在しないはず。
正格な連続関数からなるpointed CPO [A→B] は冪にはならないのかなぁ、と一瞬考えてしまったけれど、さっきの議論から簡単な反例を抽出できる。Aを2要素以上からなるpointed CPOとすると hom(0×A,0×A) ≅ hom(1×A,1×A) ≅ hom(A,A) は2個以上の要素を持つ一方で、hom(0,[A→0×A]) は1要素しか持たないので、同型にならない。
[2005-03-30 追記] ちなみに、A⊗B = {(a,b) | a∈A, b∈B, a≠⊥, b≠⊥} ∪ {⊥} と定義すると、-⊗A は [A→-] の左随伴になっている。つまり、この圏は⊗をモノイド演算とする symmetric monoidal closed category になっている。
λ. 不動点と有限直和を持つ distributive category ?
[2005-03-27 追記] ところで、最初の議論で使った 0×A ≅ 0 は distributive category の定義に含まれるので、この議論での CCC という条件は distributive category に弱めることが出来ると思う。
