2008-04-10 [長年日記]
λ. スライスがCCCのときのプルバックの右随伴
メモ。
圏Cの全てのスライスがCCCであるとき、C上の射 F: A→B からプルバックによって定義される関手 F*: C/B→C/A が右随伴 ∏F: C/A→C/B を持つことを示す。
p∈|C/A| とすると、pはCにおける dom(p)→Aという射で、C/Bの(F∘p)→Fという射でもある。
![\xymatrix{ \mathrm{dom}(p) \ar[rr]^{p} \ar[dr]_{F\circ p} & & A \ar[dl]^{F} \\ & B }](tex/7553ef7d748eff57f107903651f58c28.png "\xymatrix{ \mathrm{dom}(p) \ar[rr]^{p} \ar[dr]_{F\circ p} & & A \ar[dl]^{F} \\ & B }")
また、F∈|C/B| で C/B はCCCなので (-)F : C/B → C/B という関手が出来、これを適用すると pF : (F∘p)F → FF が得られる。 そこで、これと curry(π2) : 1 → FF とのプルバックで ∏F(p)∈|C/B| を定義する。 (C/B にプルバックが存在することは、この間の「スライスのスライスはスライス」から言える)
![\xymatrix{ \prod_F(p) \ar@{}[dr]|{\text{pb}} \ar[d] \ar[r] & (F\circ p)^F \ar[d]^{p^F} \\ 1 \ar[r]_{\mathrm{curry}(\pi_2)} & F^F }](tex/7c94a62e1cab8b2f5495183cfe4f1c4b.png "\xymatrix{ \prod_F(p) \ar@{}[dr]|{\text{pb}} \ar[d] \ar[r] & (F\circ p)^F \ar[d]^{p^F} \\ 1 \ar[r]_{\mathrm{curry}(\pi_2)} & F^F }")
そうすると、以下が自然な対応になる。
- X→∏F(p) in C/B
- f : X→(F∘p)F in C/B such that pF∘f = curry(π2)∘!
- g : X×F→(F∘p) in C/B such that p∘g = π2
- g : (F∘F*X)→(F∘p) in C/B such that p∘g = F*X
- g : F*X→p in C/A
[ツッコミを入れる]
