# Kerodon

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

Proposition 9.10.5.2. Let $\operatorname{\mathcal{C}}$ be a category and let $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ be a lax functor of $2$-categories. Then the Grothendieck construction $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ is well-defined: that is, the composition law described in Construction 9.5.0.54 is unital and associative.

Proof. We proceed as in the proof of Proposition 5.7.1.3, with some minor variations in notation. Let $(D,Y)$ be an object of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. We let $\operatorname{id}_{ (D,Y)}$ denote the morphism from $(D,Y)$ to itself given by the pair $(\operatorname{id}_{D}, \epsilon _{D}(Y) )$, where $\epsilon _{D}: \operatorname{id}_{ \mathscr {F}(D) } \rightarrow \mathscr {F}( \operatorname{id}_{D} )$ is the identity constraint for the lax functor $\mathscr {F}$. We first show that $\operatorname{id}_{(D,Y)}$ is a (two-sided) unit for the composition law on $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. We consider two cases:

• Let $(C,X)$ be another object of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ and let $(f,u): (C,X) \rightarrow (D,Y)$ be a morphism in $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. We wish to show that the composition $\operatorname{id}_{(D,Y)} \circ (f,u)$ is equal to $(f,u)$ (as a morphism from $(C,X)$ to $(D,Y)$). Unwinding the definitions, this is equivalent to the assertion that the morphism $u: X \rightarrow \mathscr {F}(f)(Y)$ is equal to the composition

$X \xrightarrow {u} \mathscr {F}(f)(Y) \xrightarrow { \mathscr {F}(f)( \epsilon _ D(Y) ) } (\mathscr {F}(f) \circ \mathscr {F}(\operatorname{id}_ D))(Y) \xrightarrow { \mu _{f, \operatorname{id}_{D} }(Y) } \mathscr {F}(f)(Y).$

This follows from the observation that the composite transformation

$\mathscr {F}(f) \xrightarrow { \epsilon _ D } \mathscr {F}(f) \circ \operatorname{id}_ D \xrightarrow { \mu _{f, \operatorname{id}_{D} } } \mathscr {F}(f)$

is the identity, which follows from axiom $(b)$ of Definition 2.2.4.5.

• Let $(E,Z)$ be another object of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$, and let $(g,v): (D,Y) \rightarrow (E,Z)$ be a morphism in $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. We wish to show that the composition $(g,v) \circ \operatorname{id}_{(D,Y)}$ is equal to $(g,v)$ (as a morphism from $(D,Y)$ to $(E,Z)$). Unwinding the definitions, this is equivalent to the assertion that the morphism $v: Y \rightarrow \mathscr {F}(g)(Z)$ is given by the upper cycle in the diagram

$\xymatrix@R =50pt@C=50pt{ Y \ar [r]^-{ \epsilon _{D}(Y) } \ar [d]^-{v} & \mathscr {F}(\operatorname{id}_ D)(Y) \ar [d]^-{ \mathscr {F}(\operatorname{id}_ D)(v) } & \\ \mathscr {F}(v)(Z) \ar [r]^-{\epsilon _ D( \mathscr {F}(v)(Z) )} & (\mathscr {F}(\operatorname{id}_ D) \circ \mathscr {F}(v))(Z) \ar [r]^-{ \mu _{\operatorname{id}_{D}, v)}(Z)} & \mathscr {F}(v)(Z). }$

Since $\epsilon _{D}$ is a natural transformation, this diagram commutes. It will therefore suffice to show that the lower composition is equal to $v$, which follows from axiom $(a)$ of Definition 2.2.4.5.

We now show that composition of morphisms in $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$ is associative. Suppose we are given a composable sequence

$(B,W) \xrightarrow { (e,t) } (C,X) \xrightarrow { (f,u) } (D,Y) \xrightarrow { (g,v) } (E,Z)$

of morphisms of $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$. Unwinding the definitions, we obtain equalities

$(g,v) \circ ( (f,u) \circ (e,t) ) = (g \circ f \circ e, w \circ \mathscr {F}(e)(u) \circ t)$

$( (g,v) \circ (f,u) ) \circ (e,t) ) = (g \circ f \circ e, w' \circ \mathscr {F}(e)(u) \circ t),$

where $w,w': (\mathscr {F}(e) \circ \mathscr {F}(f))(Y) \rightarrow \mathscr {F}(g \circ f \circ e)(Z)$ are the morphisms in the category $\mathscr {F}(B)$ given by clockwise and counterclockwise composition in the diagram

$\xymatrix@R =50pt@C=50pt{ (\mathscr {F}(e) \circ \mathscr {F}(f))(Y) \ar [r]^-{ \mu _{e,f}(Y) } \ar [d]^-{ (\mathscr {F}(e) \circ \mathscr {F}(f))(v) } & \mathscr {F}(f \circ e)(Y) \ar [d]^-{ \mathscr {F}(f \circ e)(v)} \\ (\mathscr {F}(e) \circ \mathscr {F}(f) \circ \mathscr {F}(g))(Z) \ar [d]^-{\mathscr {F}(e)(\mu _{g,f}(Z)) } \ar [r]^-{ \mu _{e,f}( \mathscr {F}(g)(Z) )} & (\mathscr {F}(f \circ e) \circ \mathscr {F}(g) )(Z) \ar [d]^-{\mu _{g,f \circ e}(Z) } \\ (\mathscr {F}(e) \circ \mathscr {F}(g \circ f)) \ar [r]^-{ \mu _{e,g\circ f}(Z) } & \mathscr {F}( g \circ f \circ e)(Z), }$

respectively. It will therefore suffice to show that this diagram commutes. For the upper square, this follows from the naturality of the composition constraint $\mu _{e,f}$. For the lower square, it follows from axiom $(c)$ of Definition 2.2.4.5. $\square$