PS

Fubini theorem in weighted limits

記法.1 @deprecated

  •  F {} _ \otimes H : \mathcal{K} \otimes \mathcal{A} \to (\mathcal{V})
  •  F {} _ \otimes H := (K,A) \mapsto FK \otimes HA
    •  F : \mathcal{K} \to (\mathcal{V})
    •  H : \mathcal{A} \to (\mathcal{V})

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

を使って

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

記法.2

  •  \textstyle\lim _ K {} ^ {FK} GK:= \lbrace F, G \rbrace
    •  F : \mathcal{K} \to (\mathcal{V})
    •  G : \mathcal{K} \to \mathcal{B}

命題

  •  \textstyle\lim _ {K,A} {} ^ { FK \otimes HA } P(K,A) \cong \lim _ A ^ {HA} \lim _ K ^ {FK} P(K,A)
    •  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)
  •  \operatorname{colim} _ K ^ {HK} \operatorname{colim} _ A ^ {FA} P(K,A) \cong \operatorname{colim} _ A ^ {FA} \operatorname{colim} _ K ^ {HK}  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}

参考文献