PS

Enriched profunctors

圏論 定義 命題 Enriched Profunctor

Symmetric closed monoidal category \mathcal{V} において･･･

Profunctor

  • H : \mathcal{B} ^ {\operatorname{op}} \otimes \mathcal{A} \to (\mathcal{V})

なる形の \mathcal{V}-erirched functor のことを

  • H : \mathcal{A} \overset{\circ}{\to} \mathcal{B}

と書き、 \mathcal{V}-enriched profunctor と呼ぶことにする。

1-category of profunctors

  • \operatorname{\mathcal{V}-\mathbf{PROF}}(\mathcal{A}, \mathcal{B}) := \operatorname{\mathcal{V}-\mathbf{CAT}}(\mathcal{B} ^ {\operatorname{op}} \otimes \mathcal{A}, (\mathcal{V}) )

Horizontal composition of profunctors

Profunctor:

  • H : \mathcal{A} \overset{\circ}{\to} \mathcal{B}
  • K : \mathcal{B} \overset{\circ}{\to} \mathcal{C}

について

  • (K \overset{\circ}\circ H)(C,A) := \textstyle\int ^ B H(B,A) \otimes K(C,B)

とすると coend-valued functor により

  • K \overset\circ\circ H : \mathcal{A} \overset{\circ}{\to} \mathcal{C}

さらに、 \mathcal{V}-natural transformation:

  • \alpha : H \Rightarrow H'
    • H, H' : \mathcal{A} \overset{\circ}{\to} \mathcal{B}
  • \beta : K \Rightarrow K'
    • K, K' : \mathcal{B} \overset{\circ}{\to} \mathcal{C}

について、coend 1-functor を使って

f:id:mbps:20151121065333p:plain

とすると、coend 1-functor の functoriality により bifunctorial。

Unitor of profunctors

Profunctor:

  • H : \mathcal{A} \overset{\circ}{\to} \mathcal{B}

について、co-Yoneda を使って

  • l := (\operatorname{Hom} _ {\mathcal{B}} \overset\circ\circ H)(C,A) \cong \textstyle\int ^ B \mathcal{B}^{\operatorname{op}}(B,C) \otimes H(\mathtt{-},A)(B) \cong _ {\text{coYoneda}} H(\mathtt{-},A)(C) = H(C,A)
  • r := (H \overset\circ\circ \operatorname{Hom} _ {\mathcal{A}})(C,A) = \textstyle\int ^ B \mathcal{A}(B,A) \otimes H(C,\mathtt{+})(B) \cong _ {\text{coYoneda}} H(C, \mathtt{+})(A) = H(C,A)

Associator of profunctors

Profunctor:

  • J : \mathcal{C} \overset{\circ}{\to} \mathcal{D}
  • H : \mathcal{B} \overset{\circ}{\to} \mathcal{C}
  • K : \mathcal{A} \overset{\circ}{\to} \mathcal{B}

について、 a :=

\begin{aligned} & ( (K \overset\circ\circ H) \overset\circ\circ J) (D,A) = \textstyle\int ^ B J(B,A) \otimes (\textstyle\int ^ C H(C,B) \otimes K(D,C) ) \\ \cong & \lbrace \otimes \text{ preserves coends} \rbrace \\ & \textstyle\int ^ B \textstyle\int ^ C ( J(B,A) \otimes H(C,B) \otimes K(D,C) ) \\ \cong & \lbrace \text{Fubini} \rbrace \\ & \textstyle\int ^ C \textstyle\int ^ B (J(B,A) \otimes H(C,B) \otimes K(D,C) ) \\ \cong & \lbrace \otimes \text{ preserves coends} \rbrace \\ & \textstyle\int ^ C ( \textstyle\int ^ B J(B,A) \otimes H(C,B) ) \otimes K(D,C) = (K \overset\circ\circ (H \overset\circ\circ J) ) (D,A) \end{aligned}

命題: Bicategory of profunctors

  • (\operatorname{\mathcal{V}-\mathbf{PROF}}, \overset\circ\circ, \operatorname{Hom}, a, l, r)

は bicategory になる。

証明

  • Unitality は coending cowedge の naturality による。
  • Associativity は coending cowedge の epi 性 による。

参考文献