Todd Trimble 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.

Lemma (Kelly)

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

Proof

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