日記 (2018 年 2 月 7 日)
これまでどこに向かって進んでるのか分からない感じのこの日記だが、 今回でようやく 1 つのメインとなる結果が出る。
以下のような圏を考える。
定義 5.1.
圏 CAAccNF を、
- 対象は、 集合 A に対して SetA という形の圏全体とする。
- 2 つの対象 SetA,SetB の間の射は、 正規関手 F:SetA→SetB の同型類全体とする。
として定義する。
奇妙な名前だが、 これは以下の定理をもとにしている。
定義 5.2.
圏 が、 4 条件
- は全ての有限極限をもつ。
- は全ての小さな余積をもち、 その余積は非交かつ普遍的である。
- 上記の 2 条件が満たされるとき Sub(1) は束の構造をもつが、 Sub(1) の原子元の全体は高々集合の大きさである。
- の任意の対象は Sub(1) の原子元の余積と同型である。
を全て満たすとき、 は完備原子的到達可能 (complete atomic accessible) であるという。
定理 5.3.
任意の完備原子的到達可能圏 に対し、 ある集合 A が存在して、 圏同値 ≅SetA が成り立つ。
さて、 ここまでの議論は以下の定理を示すのが 1 つの目標だったのである。
定理 5.4.
圏 CAAccNF はカルテシアン閉である。
証明.
CAAccNF の対象 SetA,SetB に対し、 その積と冪は、
SetA×SetB = SetA+B SetA⇀SetB = SetexpA×B
で与えられる。
積が上の形で与えられることは明らかなので、 冪が上の形で与えられることを示す。
CAAccNF の別の対象 SetC に対し、 定理 4.7 を用いると、 圏同値
[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.5.
カルテシアン閉圏 CAAccNF の冪の余単位は、
ev: SetexpA×B×SetA ⟶ SetB (M,X) ⟼ MX
で与えられる。
証明.
簡単のため 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 (上記以外)
である。
実際、 各 c∈C と M∈SetC に対し、
NcM = δ∈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 と対応するものは、 各 b∈B に対し、
Nb: SetC+A ⟶ Set Y ⟼ ϵ∈exp(C+A)(Hom(ϵ,Y)×N(ϵ,b))
で与えられるが、 これは、
Nb: SetC×SetA ⟶ Set (M,X) ⟼ γ∈expA(Hom(γ,X)×M(γ,b))
とも書ける。
実際、 最初の表示の余積においては、 γ∈expA に対して ϵ=γ∪{(γ,b)} という形の場合しか考えなくて良く、 このとき、
Hom(γ∪{(γ,b)},(M,X))≅Hom(γ,X)×M(γ,b)
が成り立つから、 上の 2 つの表示は等しい。
さらに、 上の 2 つ目の表示の右辺は MbX そのものである。
以上により、 命題が示された。
参考文献
- R. Hasegawa (2006) 「Two applications of analytic functors」 『Theoretical Computer Science』 272:113–175