Proving lemmas on monoidal categories

I will divulge some “secret recipes” a little later; for the moment I’ll just write down some coherence-theoretic diagrams which will appear shortly in the nLab (monoidal category article).

Monoidal product symbols will be suppressed, to save space.

In a monoidal category, the equation $\lambda_x y = \lambda_{x y} \circ \alpha_{I, x, y}$ holds, i.e., the diagram

$\array{
(I x) y & & \\
^\mathllap{\alpha_{I, x, y}} \downarrow & \searrow^\mathrlap{\lambda_x y} & \\
I (x y) & \underset{\lambda_{x y}}{\to} & x y
}$

commutes. Similarly, the following equation holds: $\rho_{x y} = (x \rho_y) \circ \alpha_{x, y, I}$.

We prove only the first equation; the proof of the second is entirely analogous. Since the functor $I \otimes -$ is an equivalence, it suffices to show that the triangle marked by a question mark in the diagram below commutes:

$\array{
((I I)x y) & \stackrel{\alpha_{I, I, x}y}{\to} & (I(I x)y) & \stackrel{\alpha_{I, I x, y}}{\to} & I((I x)y) & \stackrel{I\alpha_{I, x, y}}{\to} & I(I(x y)) \\
& ^\mathllap{(\rho_I x)y} \searrow & \downarrow^\mathrlap{(I \lambda_x)y} & & ^\mathllap{I(\lambda_x y)} \downarrow & ? \swarrow^\mathrlap{I(\lambda_{x y})} & \\
& & (I x)y & \underset{\alpha_{I, x, y}}{\to} & I(x y) & &
}$

where the unmarked square commutes by naturality of $\alpha$, and the unmarked triangle commutes by a unit coherence triangle (tensored by $y$ on the right). Since all the arrows are isomorphisms, it suffices to show that the diagram formed by the perimeter commutes. But this follows from the commutativity of the diagram

$\array{
& & (I(I x))y & \stackrel{\alpha_{I, I x, y}}{\to} & I((I x)y) \\
& ^\mathllap{\alpha_{I, I, x}y} \nearrow & & & \downarrow^\mathrlap{I\alpha_{I, x, y}} \\
((I I)x)y & \stackrel{\alpha_{I I, x, y}}{\to} & (I I)(x y) & \stackrel{\alpha_{I, I, x y}}{\to} & I(I(x y)) \\
^\mathllap{(\rho_I x)y} \downarrow & & ^\mathllap{\rho_I(x y)} \downarrow & \swarrow^\mathrlap{I \lambda_{x y}} & \\
(I x)y &\underset{\alpha_{I, x, y}}{\to} & I(x y) & &
}$

which uses the pentagon coherence condition, naturality of $\alpha$, and a unit coherence condition.

Created on September 11, 2012 at 18:37:36
by
Todd Trimble