Avendia19
English

日記 (2018 年 2 月 7 日)

これまでどこに向かって進んでるのか分からない感じのこの日記だが、 今回でようやく 1 つのメインとなる結果が出る。

以下のような圏を考える。

1

CAAccNF を、

として定義する。

奇妙な名前だが、 これは以下の定理をもとにしている。

2

󰒚 が、 4 条件

を全て満たすとき、 󰒚完備原子的到達可能complete atomic accessible であるという。

3

任意の完備原子的到達可能圏 󰒚 に対し、 ある集合 A が存在して、 圏同値 󰒚SetA が成り立つ。

さて、 ここまでの議論は以下の定理を示すのが 1 つの目標だったのである。

4

CAAccNF はカルテシアン閉である。

CAAccNF の対象 SetA,SetB に対し、 その積と冪は、 SetA×SetB = SetA+B SetASetB = SetexpA×B で与えられる。 積が上の形で与えられることは明らかなので、 冪が上の形で与えられることを示す。

CAAccNF の別の対象 SetC に対し、 2 月 6 日の定理 6 を用いると、 圏同値 [SetC,SetexpA×B]NF SetexpC×(expA×B) Setexp(C+A)×B [SetC+A,SetB]NF = [SetC×SetA,SetB]NF が成立することが分かる。 これはすなわち、 集合としての同型 HomCAAccNF(SetC,SetexpA×B)HomCAAccNF(SetC×SetA,SetB) が成り立つことを意味している。 したがって、 冪は上に示した形で与えられる。

これで CAAccNF のカルテシアン閉性が示されたが、 冪対象に関する上の同型がいまいち具体的にどうなっているのか分からない。 そこで、 上の証明における対象の対応を追って、 冪の余単位を具体的に計算してみる。 そうあってほしい結果がそのまま得られる。

5

カルテシアン閉圏 CAAccNF の冪の余単位は、 ev: SetexpA×B×SetA SetB (M,X) M󰂦X で与えられる。

簡単のため C:=expA×B とおく。 上の証明の圏同値 [SetC,SetC]NF SetexpC×C Setexp(C+A)×B [SetC+A,SetB]NF = [SetC×SetA,SetB]NF において、 idSetC[SetC,SetC]NF と対応するものが求めたい余単位である。

まず、 最初の圏同値で idSetC と対応するのは、 N: expC×C Set (δ,c) { 1 (δ={c}) 0 (上記以外) である。 実際、 各 cCMSetC に対し、 N󰂦cM = 󰄘δexpC(Hom(δ,M)×N(δ,c)) Hom({c},M) Mc であるから、 N󰂦=idSetC である。

次の圏同値でこの N と対応するのは、 同じ記号を使うが、 N: exp(C+A)×B Set (ϵ,b) { 1 (ϵ=γ{(γ,b)},γexpA) 0 (上記以外) である。 このことは、 全単射 expC×(expA×B) exp(C+A)×B (δ,(γ,b)) (δγ,b) を考えれば明らかである。

さらに次の圏同値でこの N と対応するものは、 各 bB に対し、 N󰂦b: SetC+A Set Y 󰄘ϵexp(C+A)(Hom(ϵ,Y)×N(ϵ,b)) で与えられるが、 これは、 N󰂦b: SetC×SetA Set (M,X) 󰄘γexpA(Hom(γ,X)×M(γ,b)) とも書ける。 実際、 最初の表示の余積においては、 γexpA に対して ϵ=γ{(γ,b)} という形の場合しか考えなくて良く、 このとき、 Hom(γ{(γ,b)},(M,X))Hom(γ,X)×M(γ,b) が成り立つから、 上の 2 つの表示は等しい。 さらに、 上の 2 つ目の表示の右辺は M󰂦bX そのものである。 以上により、 命題が示された。

参考文献

  1. R. Hasegawa (2006) 「Two applications of analytic functors」 『Theoretical Computer Science』 272:113–175