PS

(Co)ends in enriched categories

圏論 定義 命題 Enriched Power Yoneda

End

  • \textstyle\int _ A G(A,A) := \operatorname{corep} _ B \textstyle\int _ A \mathcal{B}(B,G(A,A) )
    • G : \mathcal{A} ^ {\operatorname{op}} \otimes \mathcal{A} \to \mathcal{B}
      • \mathcal{B}(B, \textstyle\int _ A G(A,A) ) \cong \textstyle\int _ A \mathcal{B}(B,G(A,A) )

特に、 \mathcal{B} := (\mathcal{V}) のとき、 \lbrack B, \unicode{0x2013} \rbrack preserves ends より記号に矛盾は無い。

Coend

  • \textstyle\int ^ A G(A,A) := \operatorname{rep} _ B \textstyle\int _ A \mathcal{B}(G(A,A),B )
    • G : \mathcal{A} ^ {\operatorname{op}} \otimes \mathcal{A} \to \mathcal{B}
      • \mathcal{B}(\textstyle\int _ A G(A,A),B ) \cong \textstyle\int _ A \mathcal{B}(G(A,A),B )

命題: (Co)ends via weighted (co)limits

証明

\begin{aligned} & \textstyle\int _ {A,A'} \lbrack \mathcal{A}(A,A'), \mathcal{B}(B,G(A,A') ) \rbrack \\ \cong & \lbrace \text{Fubini} \rbrace \\ & \textstyle\int _ A \textstyle\int _ {A'} \lbrack \mathcal{A}(A,A'), \mathcal{B}(B,G(A,A') ) \rbrack \\ \cong & \lbrace \text{Yoneda iso} \rbrace \\ & \textstyle\int _ A \mathcal{B}(B,G(A,A) ) \\ \end{aligned}

命題: (Co)powers preserve (co)ends

  • \lbrack X ,\textstyle\int _ A G(A,A) \rbrack \cong \textstyle\int _ A \lbrack X, G(A,A) \rbrack
  • X \otimes \textstyle\int ^ A G(A,A) \cong \textstyle\int _ A X \otimes G(A,A)
    • G : \mathcal{A} ^ {\operatorname{op}} \otimes \mathcal{A} \to \mathcal{B}
    • X \in \mathcal{V}

ただし、preservation of ends は (Co)ends via weighted (co)limits を通して Preservation of weighted limits - PS により定義するものとする。

証明

\begin{aligned} & \mathcal{B}(B,\lbrack X, \textstyle\int _ A G(A,A) \rbrack) \\ \cong & \lbrace \text{power} \rbrace \\ & \lbrack X, \mathcal{B}(B, \textstyle\int _ A G(A,A) ) \rbrack \\ \cong & \lbrace \text{end} \rbrace \\ & \lbrack X, \textstyle\int _ A \mathcal{B}(B,G(A,A) ) \rbrack \\ \cong & \lbrace \text{preservation of ends} \rbrace \\ & \textstyle\int _ A \lbrack X, \mathcal{B}(B,G(A,A) \rbrack \\ \cong & \lbrace \text{power} \rbrace \\ & \textstyle\int _ A \mathcal{B}(B, \lbrack X,G(A,A) \rbrack ) \\ \end{aligned}

命題: Weighted (co)limits via (co)powers

  • \operatorname{lim} ^ {FK} _ K GK \cong \textstyle\int _ K \lbrack FK,GK \rbrack
    • F : \mathcal{K} \to (\mathcal{V})
    • G : \mathcal{K} \to \mathcal{B}
  • \operatorname{colim} ^ {FK} _ K GK \cong \textstyle\int ^ K FK \otimes GK
    • F : \mathcal{K} ^ {\operatorname{op}} \to (\mathcal{V})
    • G : \mathcal{K} \to \mathcal{B}

証明

\begin{aligned} & \textstyle\int _ K \lbrack FK, \mathcal{B}(B,GK ) \rbrack \\ \cong & \lbrace \text{power} \rbrace \\ & \textstyle\int _ K \mathcal{B}(B, \lbrack FK,GK \rbrack ) \\ \end{aligned}

命題: (Co)Yoneda lemma via (co)powers

  • \textstyle\int _ L \lbrack \mathcal{K}(K,L), GL \rbrack \cong GK \cong \textstyle\int ^ L \mathcal{K}(L,K) \otimes GL
    • G: \mathcal{K} \to \mathcal{B}

証明

上記の Weighted (co)limits via (co)ends と Weighted limit による enriched Yoneda lemma - PS による。

ついに Haskell の Coyoneda が出てきた、ということになるが、なぜこの形が「たまたま」free functor になっているのかは分からない。

参考文献