Unit-copower monoidal functor

(･･･とでも呼んでみる)

以下、curry(close) bijection の箱の添字は省略する。

Copowers in 1-categories

- natural in $X$

Copower bijections

上記の natural isomorphism は copower injection:

$( e \cdot : Y \to E \cdot Y ) _ {e \in E}$

による bijection:

f:id:mbps:20150810155405p:plain

により表すことができるのであった。

命題: Closed monoidal products preserve copowers

Closed monoidal category:

- $\mathcal{V} _ 0$ has copowers.

において (left adjoints preserve colimits であったので)

$E \cdot (Y \otimes Z) \cong (E \cdot Y) \otimes Z$

証明

f:id:mbps:20150810155557p:plain

Unit-copower functor

$(\unicode{0x2013}) \cdot I : \mathcal{Set} \to \mathcal{V} _ 0$

f:id:mbps:20150810155620p:plain

命題

上記の functor は strong monoidal functor:

- $\phi : (E \cdot I) \otimes (F \cdot I) \cong ( E \times F )\cdot I$
- $\phi _ 0 : I \cong \lbrace \ast \rbrace \cdot I$

になる(と思う)。

証明

$\begin{aligned} & \mathcal{Set}(E \times F, \mathcal{V} _ 0(I,X) ) \\ \cong & \lbrace \text{curry} \rbrace \\ & \mathcal{Set}(E, \mathcal{Set}(F, \mathcal{V} _ 0(I,X) ) ) \\ \cong & \lbrace \text{copowers} \rbrace \\ & \mathcal{V} _ 0 (E \cdot (F \cdot I),X) \\ \cong & \lbrace \text{units} \rbrace \\ & \mathcal{V} _ 0(E \cdot (I \otimes (F \cdot I) ), X ) \\ \cong & \lbrace \text{preservation of copowers} \rbrace \\ & \mathcal{V} _ 0( (E \cdot I) \otimes (F \cdot I), X) \\ \end{aligned}$