Multiplication and division by a morphism under the “inner composition” in closed monoidal categories

Question

I asked this a week ago at math.stackexchange, without success, so I hope it will be appropriate here.

Let ${\mathcal C}$ be a symmetric closed monoidal category, and let me denote the internal hom-functor by a fraction $$ (X,Y)\mapsto\frac{Y}{X}, $$ so that we have an isomorphism of functors $$ \operatorname{Mor}(A\otimes B,C)\cong \operatorname{Mor}\left(A,\frac{C}{B}\right). $$ As is known, ${\mathcal C}$ is an enriched category over itself. For each objects $A,B,C$ let me denote by $\bullet_{A,B,C}$ the "inner composition" in ${\mathcal C}$ as in an enriched category, i.e. the morphism $$ \bullet_{A,B,C}:\frac{C}{B}\otimes\frac{B}{A}\to\frac{C}{A} $$ with the corresponding properties.

I wonder if the following identity always holds $$ \bullet_{A,C,D}\circ\left(1_{\frac{D}{C}}\otimes\frac{\varphi}{1_A}\right)= \bullet_{A,B,D}\circ\left(\frac{1_D}{\varphi}\otimes1_{\frac{B}{A}}\right) $$ (for arbitrary objects $A,B,C,D$ and for arbitrary morphism $\varphi:B\to C$).

This is strange, I can prove this only in the case when the unit $I$ is a separating object in ${\mathcal C}$ (what does not always hold). Is it possible that there is a counterexample?

Answer 1

Yes, this equation follows from the axioms of closed monoidal categories. I think the easiest way to prove this is to show that the corresponding pair of multimaps $\frac{D}{C}, \frac{B}{A} \to \frac{D}{A}$ are equal in any closed multicategory, which you can do by expressing them as (ordered linear) lambda terms and checking that they have the same normal form.

Let $b:B \vdash \varphi:C$ be an arbitrary term with one free variable $b$. Define two terms $t_1$ and $t_2$ of type $$ f:\frac{D}{C}, g:\frac{B}{A} \vdash t_i : \frac{D}{A} $$ by $$ t_1 := \lambda a.f ((\lambda a'.\varphi[g(a')/b])a) $$ $$ t_2 := \lambda a.(\lambda b'.f (\varphi[b'/b]))(g(a)) $$ where "$t[u/x]$" denotes the capture-avoiding substitution of the term $u$ for the variable $x$ in $t$. These correspond to the two morphisms $\bullet_{A,C,D}\circ\left(1_{\frac{D}{C}}\otimes\frac{\varphi}{1_A}\right)$ and $\bullet_{A,B,D}\circ\left(\frac{1_D}{\varphi}\otimes1_{\frac{B}{A}}\right)$, respectively, but both $t_1$ and $t_2$ normalize (after one $\beta$-reduction) to the same term $$ t = \lambda a.f (\varphi[g(a)/b]) $$ which proves that the two morphisms are equivalent modulo the equations of closed monoidal categories.

(In the above I have been implicitly treating your $\otimes$ as a comma, but if we want to be completely rigorous about this we can work with a closed representable multicategory.)

Answer 2

Noam’s answer is already good and complete, but here is alternate answer phrased more elementarily in terms of the symmetric monoidal category structure. We want to show

$$\bullet_{A,C,D}\circ\left(1_{[C,D]}\otimes[1_A,\varphi]\right)= \bullet_{A,B,D}\circ\left([\varphi,1_D]\otimes 1_{[A,B]}\right) : [C,D] \otimes [A,B] \to [A,D] $$

It’s enough to show their corresponding exponential transpose maps $[C,D] \otimes [A,B] \otimes A \to D$ agree. But for these, we have:

$$ \newcommand{\ev}{\operatorname{ev}} \ev_{A,D} \circ \left( (\bullet_{A,C,D} \circ(1_{[C,D]}\otimes[1_A,\varphi])) \otimes 1_A \right) \\ = \ev_{A,D} \circ (\bullet_{A,C,D} \otimes 1_A)\circ\left(1_{[C,D]}\otimes[1_A,\varphi] \otimes 1_A\right) \\ = \ev_{C,D} \circ (1_{[C,D]} \otimes \ev_{A,C})\circ \left(1_{[C,D]}\otimes[1_A,\varphi] \otimes 1_A\right) \\ = \ev_{C,D} \circ (1_{[C,D]} \otimes (\ev_{A,C} \circ ([1_A,\varphi] \otimes 1_A))) \\ = \ev_{C,D} \circ (1_{[C,D]} \otimes (\varphi \circ \ev_{A,B})) \\ = \ev_{C,D} \circ (1_{[C,D]} \otimes \varphi) \circ (1_{[C,D]} \otimes \ev_{A,B}) $$

and a similar calculation shows $$ \ev_{A,D} \circ \left( (\bullet_{A,B,D}\circ([\varphi,1_D]\otimes 1_{[A,B]})) \otimes 1_A \right) = \ev_{C,D} \circ (1_{[C,D]} \otimes \varphi) \circ (1_{[C,D]} \otimes \ev_{A,B}).$$

Each step is just using either the monoidal category laws, or the fact that the maps $\bullet_{A,C,D}$, $[1_A,\varphi]$ are defined by their exponential transpose maps.

(Please excuse my using the notation $[A,B]$ for mapping objects, since I’m more familiar with it than the fraction notation $\frac{B}{A}$.)