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

multiplication and division by a morphism under the inner multiplication

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

  • $\begingroup$ 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])$. $\endgroup$ Jun 30 '19 at 11:19
  • $\begingroup$ (that should be "type $\frac DC \to \frac{\frac DA}{\frac BA}$") $\endgroup$ Jun 30 '19 at 11:32
  • 1
    $\begingroup$ Noam, this is something new for me, I need some time to understand this. $\endgroup$ 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}$.)

  • $\begingroup$ Peter, I don't understand why the second calculation gives the same result. $\endgroup$ Jun 30 '19 at 13:03
  • $\begingroup$ 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]$. $\endgroup$ Jun 30 '19 at 14:23
  • $\begingroup$ 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})$? $\endgroup$ Jun 30 '19 at 14:46
  • $\begingroup$ 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. $\endgroup$ Jun 30 '19 at 14:54
  • 1
    $\begingroup$ Now all we need is for someone to give a proof with string diagrams! $\endgroup$ Jul 1 '19 at 18:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.