2007-06-06 [長年日記]
λ. CCC と *-autonomy
先日のIntroducing categories to the practicing physicistに以下のようにあったが、これはどう示すのだろう?
Proposition. A symmetric monoidal category which is both cartesian closed and *-autonomous can only be a preordered set.
まず、hom(A,B) ≅ hom(1,A⇒B) ≅ hom((A⇒B)*, 1*) ≅ hom((A⇒B)*, 0) 。 一方、CCCは分配的な圏なので 0≅0×0 であり、hom(A,B) ≅ hom((A⇒B)*, 0) ≅ hom((A⇒B)*, 0×0) ≅ hom((A⇒B)*, 0) × hom((A⇒B)*, 0) ≅ hom(A,B) × hom(A,B) となる。 ここから、hom(A,B) は空集合か一点集合か無限集合であることがわかる。 あとは無限集合でないことを言えばよいのだけど、これをどう示したらよいかわからない。
【追記】 もっと単純な話だった。 もし、f: X→0 が存在すれば、 <id, f>: X→X×0 と p: X×0→X が inverse になっている。 p ∘ <id, f> = id は明らかで、 <id, f> ∘ p = id は X×0 ≅ 0 が始対象であることから言える。 なので、X ≅ X×0 ≅ 0 。 したがって、hom(A,B) ≅ hom((A⇒B)*, 0) は空集合か一点集合。
【追記】 ところで、A⇒0 を ¬A と書くことにすると、これは CCC に A≅¬¬A を加えると縮退してしまうということを言っていていて、古典論理に対応する圏を作ることの難しさを示している。 そういえば、古典論理に対応する圏を作ることが難しいことは、檜山さんの「論理とはなにか？ (4:完) -- 論理から圏へ」のところでも言及されていた。
λ. 『λに歯がない』 森 博嗣
を読んだ。
Gシリーズは正直微妙だと思ってたけど、今回のは結構好みの話だった。
この傾向が続くといいなぁ。
