Kerodon

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

Remark 2.1.2.22. Let $\operatorname{\mathcal{C}}$ be a nonunital monoidal category. Suppose we are given objects $\mathbf{1}, \mathbf{1}' \in \operatorname{\mathcal{C}}$ together with isomorphisms

\[ \upsilon : \mathbf{1} \otimes \mathbf{1} \simeq \mathbf{1} \quad \quad \upsilon ': \mathbf{1}' \otimes \mathbf{1}' \simeq \mathbf{1}'. \]

To carry out the proof of Proposition 2.1.2.9, it is sufficient to assume that the functors

\[ \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\quad \quad X \mapsto \mathbf{1} \otimes X \]
\[ \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}\quad \quad X \mapsto X \otimes \mathbf{1}' \]

are fully faithful: the first assumption is sufficient to construct the left unit constraints of Construction 2.1.2.17, and the second is used at the end of the proof. This can be regarded as a categorical analogue of the observation that if a nonunital monoid admits a left unit $e$ and a right unit $e'$, then we must have $e = e'$.