Proof that enriched hom is a V-functor

124 Views Asked by At

Working in a category $\mathcal{C}$ enriched over a closed, symmetric, monoidal category $(\mathcal{V}, \times, *)$, with an object $U$ in $\mathcal{C}$ fixed, I'm trying to go through the details of a proof that the assignment $\mathcal{C}(-,U) : x \mapsto \mathcal{C}(x,U)$ defines a $\mathcal{V}$-functor from $\mathcal{C}^\text{op} \to \mathcal{V}$, but I'm stuck in showing that it preserves composition. According to section 1.6 in Kelly, it should follow easily from associativity.

This is as far as I've gotten: Using naturality of the adjunction $- \times \mathcal{C}(x,U) \dashv \mathcal{V}(\mathcal{C}(x,U),-)$, and defining $\mathcal{C}(-,U)_{xy} := \circ^\flat$, I know that since

$$\require{AMScd} \begin{CD} \mathcal{C}^\text{op}(y,z) \times \mathcal{C}^\text{op}(x,y) \times \mathcal{C}^\text{op}(U,x) @>{1 \times \circ}>> \mathcal{C}^\text{op}(y,z) \times \mathcal{C}^\text{op}(U,y)\\ @V{\circ \times 1}VV @VV{\circ}V \\ \mathcal{C}^\text{op}(x,z) \times \mathcal{C}^\text{op}(U,x) @>>{\circ}> \mathcal{C}^\text{op}(U,z) \end{CD}$$

commutes, the square

$$\require{AMScd} \begin{CD} \mathcal{C}^\text{op}(y,z) \times \mathcal{C}^\text{op}(x,y) @>{(1 \times \circ)^\flat}>> \mathcal{V}(\mathcal{C}^\text{op}(U,x), \mathcal{C}^\text{op}(y,z) \times \mathcal{C}^\text{op}(U,y))\\ @V{\circ}VV @VV{\circ_*}V \\ \mathcal{C}^\text{op}(x,z) @>>{\circ^\flat}> \mathcal{V}(\mathcal{C}^\text{op}(U,x), \mathcal{C}^\text{op}(U,z)) \end{CD}$$

also commutes, but it isn't quite what I need - if the rightmost edge of the second diagram was instead

$$ \mathcal{V}(\mathcal{C}^\text{op}(U,y), \mathcal{C}^\text{op}(U,z)) \times \mathcal{V}(\mathcal{C}^\text{op}(U,x), \mathcal{C}^\text{op}(U,y)) \xrightarrow{\qquad \circ \qquad} \mathcal{V}(\mathcal{C}^\text{op}(U,x), \mathcal{C}^\text{op}(U,z)),$$

then I'd be done. I don't see any obvious relationship between that map and the rightmost edge of the second diagram, so I worry that there's something simple about working with transposes of maps through adjunctions that I'm missing. Any suggestions are appreciated!

1

There are 1 best solutions below

2
On BEST ANSWER

This really is a game of adjunctions. Since $\mathcal{C}(-, U) : \mathcal{C}^{op} \rightarrow \mathcal{V}$ is the same as $\mathcal{C}^{op}(U,-) : \mathcal{C}^{op} \rightarrow \mathcal{V}$, we will work with the covariant functor $\mathcal{C}(U,-) : \mathcal{C} \rightarrow \mathcal{V}$, where $\mathcal{C}$ is a $\mathcal{V}$-category. We will denote the internal hom of $\mathcal{V}$ by $[-,-]$. Further, for all objects $a \in \mathcal{V}$, we shall denote the unit and counit of the adjunction $- \times a \dashv [a,-]$ by the same letters $d$ and $e$ respectively. Lastly, we denote the composition of the underlying category $\mathcal{V}_0$ of the monoidal category $\mathcal{V}$ by simple juxtaposition.

What you need is the commutativity of $\require{AMScd}$ \begin{CD} \mathcal{C}(y,z) \times \mathcal{C}(x,y)@>{\mathcal{C}(U,-)_{y,z} \times\text{ }\mathcal{C}(U,-)_{x,y}}>> [\mathcal{C}(U,y), \mathcal{C}(U,z)] \times [\mathcal{C}(U,x), \mathcal{C}(U,y)] \\ @V{\circ}VV @V{\circ}VV\\ \mathcal{C}(x,z) @>{\mathcal{C}(U,-)_{x,z}}>> [\mathcal{C}(U,x), \mathcal{C}(U,z)] \end{CD}

Applying to this (once for the (left arrow,bottom arrow) composite and once for the (top arrow, right arrow) composite), the naturality in $A$ of the adjunction bijection

$$\mathcal{V}(A \times \mathcal{C}(U,x), B) \cong \mathcal{V}(A, [\mathcal{C}(U,x), B])$$ yields the diagram $\require{AMScd}$ \begin{CD} \left([\mathcal{C}(U,y),\mathcal{C}(U,z)] \times [\mathcal{C}(U,x), \mathcal{C}(U,y)]\right) \times \mathcal{C}(U,x) @>{e(1 \times e)a}>> \mathcal{C}(U,z)\\ @A{\phantom{long}\left(\mathcal{C}(U,-)_{y,z} \times\text{ }\mathcal{C}(U,-)_{x,y}\right) \times 1_{\mathcal{C}(U,x)}}AA @V{1}VV \\ (\mathcal{C}(y,z) \times \mathcal{C}(x,y)) \times \mathcal{C}(U,x) @. \mathcal{C}(U,z) \\ @V{\circ \times 1_{\mathcal{C}(U,x)}}VV @A{1}AA \\ \mathcal{C}(x,z) \times \mathcal{C}(U,x) @>{\circ}>> \mathcal{C}(U,z) \end{CD} Thus, it suffices to prove the commutativity of this diagram. We will infact show that
$\require{AMScd}$ \begin{CD} \left([\mathcal{C}(U,y),\mathcal{C}(U,z)] \times [\mathcal{C}(U,x), \mathcal{C}(U,y)]\right) \times \mathcal{C}(U,x) @>{e(1 \times e)a}>> \mathcal{C}(U,z)\\ @A{\phantom{long}\left(\mathcal{C}(U,-)_{y,z} \times\text{ }\mathcal{C}(U,-)_{x,y}\right) \times 1_{\mathcal{C}(U,x)}}AA @V{1}VV \\ (\mathcal{C}(y,z) \times \mathcal{C}(x,y)) \times \mathcal{C}(U,x) @>{\circ(1 \times \circ)a}>> \mathcal{C}(U,z) \\ @V{\circ \times 1_{\mathcal{C}(U,x)}}VV @A{1}AA \\ \mathcal{C}(x,z) \times \mathcal{C}(U,x) @>{\circ}>> \mathcal{C}(U,z) \end{CD} is commutative. The bottom square is commutative since it is just associativity of the composition in $\mathcal{C}$. Thus, we just need to show that the top square commutes as well.

Now, observe that from the adjunctions $- \times \mathcal{C}(U,y) \dashv [\mathcal{C}(U,y), -]\text{ and }- \times \mathcal{C}(U,x) \dashv [\mathcal{C}(U,x), -]$,$$e(\mathcal{C}(U,-)_{y,z} \times 1_{\mathcal{C}(U,y)}) = \circ\quad\text{and}\quad e(\mathcal{C}(U,-)_{x,y} \times 1_{\mathcal{C}(U,x)}) = \circ\qquad\quad\text{(#)}\\$$

Thus, $e(1 \times e)a(\left(\mathcal{C}(U,-)_{y,z} \times\text{ }\mathcal{C}(U,-)_{x,y}\right) \times 1_{\mathcal{C}(U,x)})$

= $e(1 \times e)\left(\mathcal{C}(U,-)_{y,z} \times (\mathcal{C}(U,-)_{x,y} \times 1_{\mathcal{C}(U,x)})\right)a\quad\text{(using the naturality of the associator } a)$

= $e\left(1\mathcal{C}(U,-)_{y,z} \times e(\mathcal{C}(U,-)_{x,y} \times 1_{\mathcal{C}(U,x)})\right)a\qquad\text{(interchange law between }\times\text{ and composition in }\mathcal{V}_0)$

= $e\left(\mathcal{C}(U,-)_{y,z} \times \circ\right)a\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\text{(using (#))}$

= $e\left(\mathcal{C}(U,-)_{y,z} \times 1_{\mathcal{C}(U,y)}\right)(1 \times o)a\qquad\qquad\text{ }\qquad\text{(interchange law between }\times\text{ and composition in }\mathcal{V}_0)$

= $\circ(1 \times \circ)a\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\text{(using (#))}$