日記 (2018 年 2 月 6 日)
2 月 3 日には、 解析的関手の圏がある前層の圏と同値になることを示したが、 正規関手の圏に関しても同じようなことが成り立つ。
今回はそれについて触れていく。
解析的関手の間の射としては弱カルテシアン自然変換を考えたが、 正規関手の間の射としては以下のような自然変換を定義する。
定義 4.1.
関手 F,G:→ の間の自然変換 ν:F→G を考える。
任意の の射 u:S→T に対し、 図式
FSGSFTGTνSFuνTGu
が引き戻しであるとき、 ν はカルテシアン (cartesian) であるという。
また、 これまでは解析的関手や正規関手は Set 値のもののみを考えていたが、 これを SetB という形の圏に値をもつものに拡張する。
定義 4.2.
関手 F:SetA→SetB を考える。
任意の b∈B に対し、 関手
Fb: SetA ⟶ Set X ⟼ (FX)b
が正規であるとき、 F は正規 (normal) であるという。
さて、 今回の目的は正規関手の成す圏がある集合族の圏と同値になることを示すことだが、 実は普通に定義するとうまくいかず、 特定のカルテシアン自然変換を同一視する必要がある。
定義 4.3.
圏 [SetA,SetB]NF を、
- 対象は、 解析的関手 F:SetA→SetB 全体とする。
- 2 つの対象 F,G の間の射は、 カルテシアン自然変換 ν:F→G の以下に定義する同値類全体とする。
として定義する。
ここで、 ν,ν:F→G に対し ν と ν が同値であるとは、 任意の b∈B および任意の El(Fb) の正規対象 (X,x) に対して、 El(G) で (X,νXbx)≅(X,νXbx) が成り立つこととする。
定義 4.4.
集合 A に対し、 A の元から成る有限多重集合全体の成す集合を expA と書く。
なお、 expA は Nat(SetA) の対象全体の集合と同じだが、 expA は圏ではなくただの集合を表している。
したがって、 expA を圏と見なすときは射が恒等射だけの離散圏だと考えるので、 Nat(SetA) とは異なる圏になることに注意すること。
さて、 上で定義した正規関手が成す圏がある集合族の圏と同値になることを示すのだが、 その圏同値を与える関手を定義する。
関手 M:expA×B→Set を考え、 各 b∈B に対し、
Mb: SetA ⟶ Set X ⟼ γ∈expA(HomSetA(γ,X)×M(γ,b))
とおくと、 これは正規関手になる。
したがって、 これによって定まる関手 M:SetA→SetB も正規である。
また、 別の関手 M:expA×B→Set と自然変換 ξ:M→M を考え、 各 b∈X と X∈SetA に対し、
ξXb: MbX ⟶ MbX (f,x)@γ ⟼ (f,ξ(γ,b)x)@γ
とおくと、 自然変換 ξb:Mb→Mb が定まるが、 これはカルテシアンであることが容易に確認できる。
したがって、 これが定める自然変換 ξ:M→M もカルテシアンである。
以上の操作により、 関手
-: SetexpA×B ⟶ [SetA,SetB]NF M ⟼ M
が定まった。
これが圏同値であることを示したい。
そのために、 いくつか補題を用意する。
補題 4.5.
正規関手 F,G:SetA→Set の間のカルテシアン自然変換 ν:F→G を考える。
El(F) において (X,x) が正規対象であることと El(G) において (X,νXx) が正規対象であることは同値である。
証明.
省略するが、 後で書くかもしれない。
ノートの p5740 から p5741 までを参照。
補題 4.6.
関手 M:expA×B→Set を考え、 b∈B をとる。
El(Mb) の任意の正規対象 (X,(f,x)@γ) は、 (γ,(idγ,x)@γ) と同型である。
証明.
(X,(f,x)) は正規対象なので、 El(Mb) の図式
(X,(f,x))(X,(f,x))(γ,(idγ,x))iduf
を可換にする射 u が一意に存在する。
特に f∘u=idX である。
さらに Mb の定義によって、
(idγ,x)=(Mbu)(f,x)=(u∘f,x)
であるから、 特に u∘f=idγ が成り立つ。
すなわち、 f は同型射なので補題の主張が成り立つ。
定理 4.7.
圏同値
[SetA,SetB]NF≅SetexpA×B
が成立する。
証明.
まず、 定理 3.5 により、 上で定義した - は同型の違いを除いて対象の間の全射になっている。
また、 - が忠実であることも容易に示せる。
したがって、 - が充満であることを示せば証明が完了する。
任意にカルテシアン自然変換 ν:M→M をとる。
任意の (γ,b)∈expA×B と x∈M(γ,b) に対し、 補題 4.6 によって (γ,(idγ,x)) は El(Mb) で正規対象である。
したがって、 補題 4.5 によって (γ,νγb(idγ,x)) は El(Mb) で正規対象でもある。
再び補題 4.6 を用いれば、 ある元 y∈M(γ,b) が存在して、
(γ,νXb(idγ,x))≅(γ,(idγ,y))
が成り立つことが分かる。
このような y は一意だから、 これによって、 射
ξ(γ,b): M(γ,b) ⟶ M(γ,b) x ⟼ y
が定まり、 さらに自然変換 ξ:M→M が定まる。
ここで、 任意の (γ,b)∈expA×B および x∈M(γ,b) に対し、
(γ,νγb(idγ,x))≅(γ,(idγ,ξ(γ,b)x))≅(γ,ξXb(idγ,x))
が成り立つ。
補題 4.6 によって、 El(Mb) の正規対象は同型の違いを除いて全て (γ,(idγ,x)) の形だから、 上の同型は [SetA,SetB]NF の射として ξ=ν が成り立つことを意味している。
すなわち、 - は充満である。
- が充満であることを示すにあたって、 [SetA,SetB]NF の射の間に適当な同一視をしたことを用いたが、 この同一視をしないと上の圏同値は一般に成り立たない。
この反例は Taylor†2 によって与えられている。
まだ読んでないので私は分かっていない。
参考文献
- R. Hasegawa (2006) 「Two applications of analytic functors」 『Theoretical Computer Science』 272:113–175
- P. Taylor (1989) 「Quantitative domains, groupoids and linear logic」 『Category Theory and Computer Science』 155–181