トップ «前の日記(2008-04-09) 最新 次の日記(2008-04-11)» 月表示 編集

日々の流転


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 }

また、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 }

そうすると、以下が自然な対応になる。

  • 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
Tags: 圏論