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 λ xy=λ xyα I,x,y\lambda_x y = \lambda_{x y} \circ \alpha_{I, x, y} holds, i.e., the diagram

(Ix)y α I,x,y λ xy I(xy) λ xy xy\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: ρ xy=(xρ y)α x,y,I\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 II \otimes - is an equivalence, it suffices to show that the triangle marked by a question mark in the diagram below commutes:

((II)xy) α I,I,xy (I(Ix)y) α I,Ix,y I((Ix)y) Iα I,x,y I(I(xy)) (ρ Ix)y (Iλ x)y I(λ xy) ? I(λ xy) (Ix)y α I,x,y I(xy) \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 yy 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

(I(Ix))y α I,Ix,y I((Ix)y) α I,I,xy Iα I,x,y ((II)x)y α II,x,y (II)(xy) α I,I,xy I(I(xy)) (ρ Ix)y ρ I(xy) Iλ xy (Ix)y α I,x,y I(xy) \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