RAPL - PS

@deprecated

代わりに RAPL in string diagrams - PS を参照。

記法.1

$\lim _ j D _ j$ の limiting cone を

$\lim D _ j : \operatorname{lim} _ j D _ j \to D _ j$

それへの mediator を

$D _ j \langle \mu _ j \rangle$

と書いてしまうことにする。

記法.2

$Px \operatorname{op} _ x Qx \iff (\forall x)(Px \operatorname{op} Qx)$

命題

Right Adjoints Preserve Limits:

adjunction
- $F : \mathcal{C} \to \mathcal{D}$
- $U : \mathcal{D} \to \mathcal{C}$
- $\mathcal{D}(FC, D) \overset{\dashv}{\underset{\vdash}{\cong}} \mathcal{C}(C, UD)$

について

- $D : \mathcal{J} \to \mathcal{D}$

ならば

$U(\operatorname{lim} _ j D _ j) \cong \exists \operatorname{lim} _ j UD _ j$

証明.1

$\begin{aligned} & U(\operatorname{lim} D _ j : \operatorname{lim} _ j D _ j \to D _ j) \circ (f: C \to U(\operatorname{lim} _ j D _ j) ) = _ j \mu _ j : C \to U D _ j \\ \iff & \lbrace \text{Yoneda embedding is fully faithful} \rbrace \\ & \mathcal{C}(X, U(\operatorname{lim} D _ j) ) \circ \mathcal{C}(X,f) = _ {j,X} \mathcal{C}(X, \mu _ j) \\ \iff & \lbrace \text{bijectivity of } {\dashv} \rbrace \\ & {\vdash} \circ \mathcal{C}(X, U(\operatorname{lim} D _ j) ) \circ \mathcal{C}(X,f) = _ {j,X} {\vdash} \circ \mathcal{C}(X, \mu _ j) \\ \iff & \lbrace \text{naturality of } {\vdash} \rbrace \\ & \mathcal{D}(FX, \operatorname{lim} D _ j) \circ {\vdash} \circ \mathcal{C}(X,f) = _ {j,X} {\vdash} \circ \mathcal{C}(X, \mu _ j) \\ \iff & \lbrace \text{hom functors preserve limits;universality} \rbrace \\ & {\vdash} \circ \mathcal{C}(X,f) = _ X \mathcal{D}(FX, D _ j) \langle {\vdash} \circ \mathcal{C}(X, \mu _ j) \rangle \\ \iff & \lbrace \text{bijectivity of } {\dashv} \rbrace \\ & \mathcal{C}(X,f) = _ X {\dashv} \circ \mathcal{D}(FX, D _ j) \langle {\vdash} \circ \mathcal{C}(X, \mu _ j) \rangle \\ \iff & \lbrace \text{Yoneda embedding is fully faithful} \rbrace \\ & f = Y ^ {-1} ( ({\dashv} \circ \mathcal{D}(FX,D _ j) \langle {\vdash} \circ \mathcal{C}(X, \mu _ j) \rangle ) _ X ) \\ \end{aligned}$

よって Universality - PS より。

証明.2

Category Theory (Oxford Logic Guides) では

$\begin{aligned} & \mathcal{C}(X, U(\operatorname{lim} _ j D _ j) ) \\ \cong & \lbrace \text{adjunction} \rbrace \\ & \mathcal{D}(FX, \operatorname{lim} _ j D _ j) \\ \cong & \lbrace \text{hom functors preserve limits} \rbrace \\ & \operatorname{lim} _ j \mathcal{D}(FX, D _ j) \\ \cong & \lbrace \text{adjunction} \rbrace \\ & \operatorname{lim} _ j \mathcal{C}(X, UD _ j) \\ \cong & \lbrace \text{hom functors preserve limits} \rbrace \\ & \mathcal{C}(X, \operatorname{lim} _ j UD _ j) \\ \end{aligned}$