Fubini theorem in weighted limits

記法.1 @deprecated

$F {} _ \otimes H : \mathcal{K} \otimes \mathcal{A} \to (\mathcal{V})$
- $F : \mathcal{K} \to (\mathcal{V})$
- $H : \mathcal{A} \to (\mathcal{V})$

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

を使って

$F {} _ \otimes H := \operatorname{Ten} \circ (F \otimes H)$

記法.2

- $F : \mathcal{K} \to (\mathcal{V})$
- $G : \mathcal{K} \to \mathcal{B}$

命題

- $F : \mathcal{K} \to (\mathcal{V})$
- $H : \mathcal{A} \to (\mathcal{V})$
- $P : \mathcal{K} \otimes \mathcal{A} \to \mathcal{B}$

証明

$\begin{aligned} & \mathcal{B}(B, \textstyle\lim _ {K,A} ^ { FK \otimes HA } P(K,A) ) \\ \cong & \lbrace \text{definition of limits} \rbrace \\ & \textstyle\int _ {K,A} \lbrack FK \otimes HA, \mathcal{B}(B, P(K,A) ) \rbrack \\ \cong & \lbrace \text{symmetry} \rbrace \\ & \textstyle\int _ {K,A} \lbrack HA \otimes FK, \mathcal{B}(B, P(K,A) ) \rbrack \\ \cong & \lbrace \text{curry} \rbrace \\ & \textstyle\int _ {K,A} \lbrack HA, \lbrack FK, \mathcal{B}(B,P(K,A) ) \rbrack \rbrack \\ \cong & \lbrace \text{Fubini} \rbrace \\ & \textstyle\int _ A \textstyle\int _ K \lbrack HA, \lbrack FK, \mathcal{B}(B,P(K,A) ) \rbrack \rbrack \\ \cong & \lbrace \operatorname{Hom} _ {(\mathcal{V})} \text{preserves ends} \rbrace \\ & \textstyle\int _ A \lbrack HA, \int _ K \lbrack FK, \mathcal{B}(B, P(K,A) ) \rbrack \rbrack \\ \cong & \lbrace \text{definition of limits} \rbrace \\ & \mathcal{B}(B, \textstyle\lim _ A ^ {HA} \textstyle\lim _ K ^ {FK} P(K,A) ) \\ \end{aligned}$

系

$\textstyle\lim _ K ^ {HA} \textstyle\lim _ A ^ {FA} P(K,A) \cong \textstyle\lim _ A ^ {FA} \textstyle\lim _ K ^ {HK} P(K,A)$

Dual

$\operatorname{colim} _ {K,A} ^ { FK \otimes HA } P(K,A) \cong \operatorname{colim} _ A ^ {HA} \operatorname{colim} _ K ^ {FK} P(K,A)$
- $F : \mathcal{K} ^ {\operatorname{op}} \to (\mathcal{V})$
- $H : \mathcal{A} ^ {\operatorname{op}} \to (\mathcal{V})$
- $P : \mathcal{K} \otimes \mathcal{A} \to \mathcal{B}$

証明 @deprecated

$\begin{aligned} & \operatorname{colim} _ {K,A} {} ^ { F {} _ \otimes H } P(K,A) \\ = & \lbrace \text{definition of colimits} \rbrace \\ & \big( \operatorname{lim} _ { (K,A) ^ \ast } ^ {F {} _ \otimes H} (P (K,A) ) ^ \ast \big) ^ \ast = \big( \operatorname{lim} _ { K ^ \ast,A ^ \ast } ^ {F {} _ \otimes H} (P (K,A) ) ^ \ast \big) ^ \ast \\ \cong & \lbrace \text{dual} \rbrace \\ & \big( \operatorname{lim} _ {A ^ \ast } ^ H \operatorname{lim} _ {K ^ \ast} ^ F ( P(K,A) ) ^ \ast \big) ^ \ast \\ \cong & \lbrace \text{definition of colims} \rbrace \\ & \big( \operatorname{lim} _ {A ^ \ast } ^ H ( \operatorname{colim} _ {K} ^ F P(K,A) ) ^ \ast \big) ^ \ast \\ \cong & \lbrace \text{definition of colimits} \rbrace \\ & \big( \operatorname{colim} _ {A} ^ H \operatorname{colim} _ {K} ^ F P(K,A) \big) ^ {\ast\ast} = \operatorname{colim} _ {A} ^ H \operatorname{colim} _ {K} ^ F P(K,A) \end{aligned}$

参考文献

Basic Concepts of Enriched Category Theory (3.3)