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

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?

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.)

• Re: the last parenthetical, this equation can actually be generalized to any closed (not necessarily monoidal) category after currying the two morphisms to have type $\frac CB \to \frac{\frac CA}{\frac CB}$. The argument above still works, with the two corresponding terms reducing to the same normal form $\lambda g.\lambda a.f(\phi[g(a)/b])$. – Noam Zeilberger Jun 30 '19 at 11:19
• (that should be "type $\frac DC \to \frac{\frac DA}{\frac BA}$") – Noam Zeilberger Jun 30 '19 at 11:32
• Noam, this is something new for me, I need some time to understand this. – Sergei Akbarov Jun 30 '19 at 11:38

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}$$.)

• Peter, I don't understand why the second calculation gives the same result. – Sergei Akbarov Jun 30 '19 at 13:03
• Notice that in the first calculation, the two key steps use the equalities $ev_{A,D}( \bullet_{A,C,D} \otimes 1_A) = ev_{C,D} \circ (1_{[C,D]} \otimes ev_{A,C})$ and $ev_{A,C} \circ ([1_A,\varphi] \otimes 1_A) = \varphi \circ ev_{A,B}$. These equalities are essentially the definitions of $\bullet_{A,C,D}$ and $[1_A,\varphi]$ in terms of their exponential transpose maps. All other steps are just monoidal category laws. The second calculation is very analogous, but its two key steps use the defining equalities of $\bullet_{A,B,D}$ and $[\varphi,1_D]$. – Peter LeFanu Lumsdaine Jun 30 '19 at 14:23
• I don't understand something. I come to the result $\operatorname{ev}_{B,D}\circ[\varphi,1_D]\otimes\operatorname{ev}_{A,B}$. Why is this equal to $\operatorname{ev}_{C,D} \circ (1_{[C,D]} \otimes \varphi) \circ (1_{[C,D]} \otimes\operatorname{ev}_{A,B})$? – Sergei Akbarov Jun 30 '19 at 14:46
• In the result you reached, split up $([\varphi,1_D] \otimes ev_{A,B})$ as $([\varphi,1_D] \otimes 1_B) \circ (1_{[C,D]} \otimes ev_{A,B})$, and then use the defining equation of $[\varphi,1_D]$. The way to find this is to notice that you should expect to need the defining equation of $[\varphi,1_D]$, so look at that equation, and then try to think how to get your result into a form where you can use that equation. – Peter LeFanu Lumsdaine Jun 30 '19 at 14:54
• Now all we need is for someone to give a proof with string diagrams! – Mike Shulman Jul 1 '19 at 18:27