Kerodon

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

Definition 2.1.5.2. Let $\operatorname{\mathcal{C}}$ and $\operatorname{\mathcal{D}}$ be monoidal categories with unit objects $\mathbf{1}_{\operatorname{\mathcal{C}}}$ and $\mathbf{1}_{\operatorname{\mathcal{D}}}$, respectively. Let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a nonunital lax monoidal functor with tensor constraints $\mu = \{ \mu _{X,Y} \} _{X,Y \in \operatorname{\mathcal{C}}}$. Let $\epsilon : \mathbf{1}_{\operatorname{\mathcal{D}}} \rightarrow F(\mathbf{1}_{\operatorname{\mathcal{C}}})$ be a morphism in $\operatorname{\mathcal{D}}$. We say that $\epsilon $ is a left unit for $F$ if, for every object $X \in \operatorname{\mathcal{C}}$, the left unit constraint $\lambda _{F(X)}: \mathbf{1}_{\operatorname{\mathcal{D}}} \otimes F(X) \xrightarrow {\sim } F(X)$ in the category $\operatorname{\mathcal{D}}$ is equal to the composition

\[ \mathbf{1}_{\operatorname{\mathcal{D}}} \otimes F(X) \xrightarrow { \epsilon \otimes \operatorname{id}_{F(X)}} F( \mathbf{1}_{\operatorname{\mathcal{C}}} ) \otimes F(X) \xrightarrow { \mu _{ \mathbf{1}_{\operatorname{\mathcal{C}}}, X} } F( \mathbf{1}_{\operatorname{\mathcal{C}}} \otimes X) \xrightarrow { F( \lambda _ X) } F(X), \]

where $\lambda _ X: \mathbf{1}_{\operatorname{\mathcal{C}}} \otimes X \xrightarrow {\sim } X$ is the left unit constraint in the monoidal category $\operatorname{\mathcal{C}}$. We say that $\epsilon $ is a right unit for $F$ if, for every object $X \in \operatorname{\mathcal{C}}$, the right unit constraint $\rho _{F(X)}: F(X) \otimes \mathbf{1}_{\operatorname{\mathcal{D}}} \xrightarrow {\sim } F(X)$ is equal to the composition

\[ F(X) \otimes \mathbf{1}_{\operatorname{\mathcal{D}}} \xrightarrow { \operatorname{id}_{F(X)} \otimes \epsilon } F(X) \otimes F( \mathbf{1}_{\operatorname{\mathcal{C}}}) \xrightarrow { \mu _{X, \mathbf{1}_{\operatorname{\mathcal{C}}}} } F( X \otimes \mathbf{1}_{\operatorname{\mathcal{C}}} ) \xrightarrow { F( \rho _{X} ) } F(X). \]

We say that $\epsilon $ is a unit for $F$ if it is both a left and a right unit for $F$.