Kerodon

Proof. We verify each axiom in turn:

$(a)$

Let $g: B \rightarrow C$ be a morphism in the category $\operatorname{\mathcal{C}}$. We must show that the composition

\[ g^{\ast } = \operatorname{id}_{ \operatorname{\mathcal{E}}_{B} } \circ g^{\ast } \xrightarrow { \epsilon _{B} } \operatorname{id}_{B}^{\ast } \circ g^{\ast } \xrightarrow { \mu _{\operatorname{id}_ B, g} } (g \circ \operatorname{id}_{B} )^{\ast } = g^{\ast } \]

is the identity transformation from $g^{\ast }$ to itself. For every object $X \in \operatorname{\mathcal{E}}_{C}$, the commutativity of the diagram

\[ \xymatrix@R =50pt@C=50pt{ \operatorname{id}_{B}^{\ast }( g^{\ast }(X) ) \ar [r]^-{ \widetilde{ ( \operatorname{id}_{B} )}_{ g^{\ast }(X)}} \ar [d]^-{ \widetilde{ ( \operatorname{id}_{B} )}_{ g^{\ast }(X) }} & g^{\ast }(X) \ar [d]^-{ \widetilde{g}_{X} } \\ g^{\ast }(X) \ar [r]^-{ \widetilde{g}_{X} } & X } \]

shows that $\mu _{ \operatorname{id}_{B}, g}(X) = \widetilde{ ( \operatorname{id}_{B} )}_{ g^{\ast }(X)}$. The desired result now follows from the observation that $\epsilon _{B}$ carries $g^{\ast }(X)$ to the inverse $\widetilde{ ( \operatorname{id}_{B} )}_{ g^{\ast }(X)}^{-1}$.

$(b)$

Let $g: B \rightarrow C$ be a morphism in the category $\operatorname{\mathcal{C}}$. We must show that the composition

\[ g^{\ast } = g^{\ast } \circ \operatorname{id}_{ \operatorname{\mathcal{E}}_{C} } \xrightarrow { \epsilon _{C} } g^{\ast } \circ \operatorname{id}_{C}^{\ast } \xrightarrow { \mu _{g, \operatorname{id}_ C} } (\operatorname{id}_ C \circ g)^{\ast } = g^{\ast } \]

is the identity transformation from $g^{\ast }$ to itself. For every object $X \in \operatorname{\mathcal{E}}_{C}$, the commutativity of the diagram

\[ \xymatrix@R =50pt@C=50pt{ g^{\ast }( \operatorname{id}_{C}^{\ast } X) \ar [r]^-{ \widetilde{g}_{\operatorname{id}_{C}^{\ast }(X)} } \ar [d]^-{ g^{\ast }( \epsilon _{C}(X)^{-1}) } & \operatorname{id}_{C}^{\ast }(Y) \ar [d]^-{ \epsilon _{C}(X)^{-1} } \\ g^{\ast }(X) \ar [r]^-{ \widetilde{g}_{X} } & X } \]

shows that $\mu _{g,\operatorname{id}_ C}$ carries $X$ to the inverse of the morphism $g^{\ast }(\epsilon _{C}(X))$.

$(c)$

Let $f: A \rightarrow B$, $g: B \rightarrow C$, and $h: C \rightarrow D$ be composable morphisms in the category $\operatorname{\mathcal{C}}$. We wish to show that the diagram of natural transformations

\[ \xymatrix@R =50pt@C=50pt{ f^{\ast } \circ g^{\ast } \circ h^{\ast } \ar [r]^-{ f^{\ast }( \mu _{g,h} ) } \ar [d]^-{ \mu _{f,g} } & (g \circ f)^{\ast } \circ h^{\ast } \ar [d]^-{ \mu _{g \circ f, h}} \\ f^{\ast } \circ (h \circ g)^{\ast } \ar [r]^-{ \mu _{f, h \circ g} } & (h \circ g \circ f)^{\ast } } \]

is commutative. Fix an object $Y \in \operatorname{\mathcal{E}}_{D}$. We wish to show that the back face of the cubical diagram

\[ \xymatrix@C =40pt@R=60pt{ f^{\ast }(g^{\ast }(h^{\ast }(Y) ) ) \ar [rr]^{ f^{\ast }( \mu _{g,h}(Y) ) } \ar [dd]^{ \mu _{f,g}( h^{\ast }(Y)) } \ar [dr]_{ \widetilde{f}_{ g^{\ast }(h^{\ast }(Y) )} } & & f^{\ast }( (h \circ g)^{\ast } Y) \ar [dd]^(.6){ \mu _{f, h \circ g}(Y)} \ar [dr]_{ \widetilde{f}_{(h \circ g)^{\ast }(Y) } } & \\ & g^{\ast }(h^{\ast }(Y)) \ar [rr]^(.4){ \mu _{g,h}(Y) } \ar [dd]^(.6){ \mu _{g \circ f, h}(Y) } & & (h \circ g)^{\ast }(Y) \ar [dd]^{ \widetilde{(h \circ g)}_{Y} } \\ (g \circ f)^{\ast }(h^{\ast }(Y)) \ar [rr]^(.4){ \mu _{g \circ f, h}(Y) } \ar [dr]_{ \widetilde{g \circ f}_{ h^{\ast }(Y)} } & & (h \circ g \circ f)^{\ast }(Y) \ar [dr]_{ \widetilde{(h \circ g \circ f)}_{Y} } & \\ & h^{\ast }(Y) \ar [rr]^{ \widetilde{h}_{Y} } & & Y } \]

is commutative. Note that the left face commutes by the definition of $\mu _{f,g}$, the right face by the definition of $\mu _{f, h \circ g}$, the top face by the definition of the functor $f^{\ast }$, the bottom face by the definition of $\mu _{g \circ f, h}$, and the front face by the definition of $\mu _{g \circ f, h}$. Since the morphism $\widetilde{ h \circ g \circ f}_{Y}$ is locally $U$-cartesian, it follows that the back face commutes as well.