Kerodon

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

Proposition 2.1.2.9 (Uniqueness of Units). Let $\operatorname{\mathcal{C}}$ be a nonunital monoidal category equipped with units $( \mathbf{1}, \upsilon )$ and $( \mathbf{1}', \upsilon ')$ (in the sense of Definition 2.1.2.5). Then there is a unique isomorphism $u: \mathbf{1} \xrightarrow {\sim } \mathbf{1}'$ for which the diagram

$\xymatrix@R =50pt@C=50pt{ \mathbf{1} \otimes \mathbf{1} \ar [d]^-{u \otimes u} \ar [r]^-{ \upsilon } & \mathbf{1} \ar [d]^{u} \\ \mathbf{1'} \otimes \mathbf{1'} \ar [r]^-{ \upsilon '} & \mathbf{1'} }$

commutes.

Proof of Proposition 2.1.2.9. Let $\operatorname{\mathcal{C}}$ be a nonunital monoidal category equipped with units $(\mathbf{1}, \upsilon )$ and $(\mathbf{1}', \upsilon ')$. We can then regard $\operatorname{\mathcal{C}}$ as a monoidal category with unit object $\mathbf{1}$ and unit constraint $\upsilon$. For each object $X \in \operatorname{\mathcal{C}}$, let $\lambda _{X}: \mathbf{1} \otimes X \xrightarrow {\sim } X$ be the left unit constraint of Construction 2.1.2.17. We wish to show that there is a unique isomorphism $u: \mathbf{1} \simeq \mathbf{1}'$ for which the outer rectangle in the diagram of isomorphisms

$\xymatrix@C =50pt@R=50pt{ \mathbf{1} \otimes \mathbf{1} \ar [r]^-{ \lambda _{ \mathbf{1} } } \ar [d]^{ \operatorname{id}_{ \mathbf{1} } \otimes u } & \mathbf{1} \ar [d]^{u} \\ \mathbf{1} \otimes \mathbf{1}' \ar [r]^-{ \lambda _{ \mathbf{1}' }} \ar [d]^{u \otimes \operatorname{id}_{ \mathbf{1}' }} & \mathbf{1}' \ar [d]^{\operatorname{id}_{ \mathbf{1}' }} \\ \mathbf{1}' \otimes \mathbf{1}' \ar [r]^-{ \upsilon ' } & \mathbf{1}' }$

is commutative. Since the upper square commutes (Remark 2.1.2.18), this is equivalent to the commutativity of the lower square. The existence and uniqueness of $u$ now follows from the assumption that the functor $X \mapsto X \otimes \mathbf{1}'$ is fully faithful. $\square$