Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Proposition 2.1.2.19 (The Triangle Identity). Let $\operatorname{\mathcal{C}}$ be a monoidal category with unit object $\mathbf{1}$. Let $X$ and $Y$ be objects of $\operatorname{\mathcal{C}}$, and let $\rho _{X}: X \otimes \mathbf{1} \simeq X$ and $\lambda _{Y}: \mathbf{1} \otimes Y \rightarrow Y$ be the right and left unit constraints of Construction 2.1.2.17. Then the diagram of isomorphisms

\[ \xymatrix { X \otimes (\mathbf{1} \otimes Y) \ar [rr]^-{\alpha _{X, \mathbf{1}, Y} }_{\sim } \ar [dr]_{ \operatorname{id}_ X \otimes \lambda _ Y}^{\sim } & & (X \otimes \mathbf{1}) \otimes Y \ar [dl]^{ \rho _{X} \otimes \operatorname{id}_ Y}_{\sim } \\ & X \otimes Y & } \]

is commutative.

Proof. We have a diagram of isomorphisms

\[ \xymatrix@R =50pt@C=-15pt{ & X \otimes ( (\mathbf{1} \otimes \mathbf{1}) \otimes Y) ) \ar [rr]^{\alpha } \ar [d]^{\upsilon _{Y}} & & (X \otimes ( \mathbf{1} \otimes \mathbf{1} ) ) \otimes Y \ar [d]_{\upsilon _{Y} } \ar [ddr]^{\alpha } & \\ & X \otimes (\mathbf{1} \otimes Y) \ar [rr]^{ \alpha } \ar [d]^{\alpha } & & (X \otimes \mathbf{1}) \otimes Y \ar [dll]^{ \operatorname{id}} & \\ X \otimes (\mathbf{1} \otimes (\mathbf{1} \otimes Y) ) \ar [uur]^{\alpha } \ar [ur]_{\lambda _ Y} \ar [drr]^{ \alpha } & (X \otimes \mathbf{1}) \otimes Y \ar [r]^-{ \rho _{X}} & X \otimes Y & X \otimes ( \mathbf{1} \otimes Y) \ar [l]_-{ \lambda _ Y} \ar [u]_{ \alpha } & ((X \otimes \mathbf{1}) \otimes \mathbf{1}) \otimes Y \ar [ul]_{\rho _ X} \\ & & (X \otimes \mathbf{1}) \otimes (\mathbf{1} \otimes Y). \ar [ul]_{ \lambda _ Y } \ar [ur]^{ \rho _ X } \ar [urr]^{ \alpha } & & } \]

Here the outer cycle commutes by the pentagon identity $(P)$ of Definition 2.1.1.5, the upper rectangle and outer quadrilaterals by the functoriality of the associativity constraint, the side triangles by the definition of the left and right unit constraints, and the lower quadrilateral by the functoriality of the tensor product $\otimes $. It follows that the middle square is also commutative, which is equivalent to the statement of Proposition 2.1.2.19. $\square$