PS

Pointwise weighted limits

圏論 命題 Enriched Weighted limit

Currying の記法 @deprecated

\mathcal{V}-functor:

  • P : \mathcal{K} \otimes \mathcal{A} \to \mathcal{B}

について、curry isomorphism により対応する \mathcal{V}-functor:

  • \tilde{P} : \mathcal{K} \to \lbrack \mathcal{A}, \mathcal{B} \rbrack

を

  • K \mapsto A \mapsto P(K,A)

と書くことに(勝手に)する。

Lambda 記法

Lambda 記法 - PS を参照。

命題

\mathcal{V}-functor:

  • F: \mathcal{K} \to (\mathcal{V})
  • P : \mathcal{K} \otimes \mathcal{A} \to \mathcal{B}

について、weighted limit の族:

  • \big( \operatorname{lim} _ K ^ {FK} P(K,A) \big) _ A

が存在するならば

  • \operatorname{lim} _ K ^ {FK} \lambda _ A P(K,A) \cong \lambda _ A \operatorname{lim} _ K ^ {FK} P(K,A)

(右辺は Enriched representability - PS の命題により定まる \mathcal{V}-functor \mathcal{A} \to \mathcal{B} のこと)

証明

\begin{aligned} & \lbrack \mathcal{A}, \mathcal{B} \rbrack (H, \lambda _ A \operatorname{lim} _ K ^ {FK} P(K,A) ) \\ \cong & \lbrace \text{definition of functor categories} \rbrace \\ & \displaystyle\int _ A \mathcal{B}(HA, \operatorname{lim} _ K ^ {FK} P(K,A) ) \\ \cong & \lbrace \text{definition of limits} \rbrace \\ & \displaystyle\int _ A \lbrack \mathcal{K}, (\mathcal{V}) \rbrack \big(F, \lambda _ K \mathcal{B}(HA, P(K,A) ) \big) \\ \cong & \lbrace \text{definition of functor categories} \rbrace \\ & \displaystyle\int _ A \displaystyle\int _ K \lbrack FK, \mathcal{B}(HA, P(K,A) ) \rbrack \\ \cong & \lbrace \text{Fubini theorem}; \operatorname{Hom} _ {(\mathcal{V})} \text{preserves ends} \rbrace \\ & \displaystyle\int _ K \lbrack FK, \displaystyle\int _ A \mathcal{B}(HA, P(K,A) ) \rbrack \\ \cong & \lbrace \text{definition of functor categories} \rbrace \\ & \lbrack \mathcal{K}, (\mathcal{V}) \rbrack \big( F, \lambda _ K \lbrack \mathcal{A}, \mathcal{B} \rbrack (H, \lambda _ A P(K,A) ) \big) \\ \end{aligned}

実装

f:id:mbps:20150828034603p:plain

記法 @deprecated

  • \lbrace F, K \mapsto A \mapsto P(K,A) \rbrace A \cong \lbrace F, K \mapsto P(K,A) \rbrace
  • (\displaystyle\lim _ K {} ^ F PK)A \cong \displaystyle\lim _ K {} ^ F ( (PK)A)

参考文献