Kerodon

Proof of Theorem 2.3.5.6. Let $\operatorname{\mathcal{C}}$ be a strict $2$-category, let $Q$ be a partially ordered set, and let $F: Q \rightarrow \operatorname{\mathcal{C}}$ be a strictly unitary lax functor. We wish to show that $F$ factors uniquely as a composition

where $T_{Q}$ is the strictly unitary lax functor of Construction 2.3.5.4 and $F^{+}$ is a strict functor from $\operatorname{Path}_{(2)}[Q]$ to $\operatorname{\mathcal{C}}$.

For every pair of elements $x,y \in Q$ satisfying $x \leq y$, we let $e_{y,x}: x \rightarrow y$ denote the unique morphism from $x$ to $y$ in the category $Q$, and for every triple $x,y,z \in Q$ satisfying $x \leq y \leq z$, we let $\mu _{z,y,x}: F( e_{z,y} ) \circ F( e_{y,x} ) \Rightarrow F( e_{z,x} )$ denote the composition constraint for the lax monoidal functor $F$. Unwinding the definitions, we see that a strict functor $F^{+}: \operatorname{Path}_{(2)}[Q] \rightarrow \operatorname{\mathcal{C}}$ satisfies $F^{+} \circ T_{Q} = F$ if and only if the following conditions are satisfied:

$(0)$

For every element $x \in Q$, we have $F^{+}(x) = F(x)$ (as objects of the $2$-category $\operatorname{\mathcal{C}}$).

$(1)$

For every pair of elements $x,y \in Q$ satisfying $x \leq y$, we have $F^{+}( \{ y, x\} ) = F( e_{y,x} )$ (as $1$-morphisms from $F(x)$ to $F(y)$ in the strict $2$-category $\operatorname{\mathcal{C}}$).

$(2)$

For every triple of elements $x,y,z \in Q$ satisfying $x \leq y \leq z$, the functor $F^{+}$ carries the inclusion $\{ z, x \} \subseteq \{ z,y,x \} $ (regarded as a $2$-morphism from $\{ z, y\} \circ \{ y,x\} $ to $\{ z, x\} $ in the strict $2$-category $\operatorname{Path}_{(2)}[Q]$) to $\mu _{z,y,x}$ (regarded as a $2$-morphism from $F( e_{z,y} ) \circ F( e_{ y,x} )$ to $F( e_{z,x} )$ in the strict $2$-category $\operatorname{\mathcal{C}}$).

Note that, since we are requiring $F^{+}$ to be a strict functor, we can replace $(1)$ by the following stronger condition:

$(1')$

For every nonempty finite linearly ordered subset $S = \{ x_0 < x_1 < \cdots < x_ n \} \subseteq Q$, the functor $F^{+}$ carries $S$ (regarded as a $1$-morphism from $x_0$ to $x_ n$ in the strict $2$-category $\operatorname{Path}_{(2)}[Q]$) to the composition $F( e_{ x_{n}, x_{n-1} } ) \circ \cdots \circ F( e_{ x_{1}, x_0} )$ (regarded as a $1$-morphism from $F( x_0)$ to $F(x_ n)$ in the strict $2$-category $\operatorname{\mathcal{C}}$). In what follows, we will denote this composition by $F(S)$.

Let $S = \{ x_0 < x_1 < \cdots < x_ n \} $ be a nonempty finite linearly ordered subset of $Q$. For each $0 \leq i \leq j \leq n$, set $f_{j,i} = F( e_{ x_ j, x_ i} )$, which we regard as a $1$-morphism from $F( x_ i )$ to $F(x_ j)$ in the $2$-category $\operatorname{\mathcal{C}}$. Let $x_ i$ be an element of $S$ which is neither the largest nor the smallest (so that $0 < i < n$). In this case, we let $\gamma _{S, x_ i}: F( S ) \Rightarrow F(S \setminus \{ x_ i \} )$ denote the $2$-morphism of $\operatorname{\mathcal{C}}$ given by the horizontal composition

More generally, given a sequence of distinct elements $s_1, s_2, \cdots , s_ m \in S \setminus \{ x_0, x_ n \} $, we let $\gamma _{ S, s_1, \ldots , s_ m }: F(S) \Rightarrow F( S \setminus \{ s_1, \ldots , s_ m \} )$ denote the $2$-morphism of $\operatorname{\mathcal{C}}$ given by the vertical composition

Since the strict functor $F^{+}$ is required to be compatible with vertical and horizontal composition, we can replace $(2)$ by the following stronger condition:

$(2')$

Let $S = \{ x_0 < x_1 < \cdots < x_ n \} $ be a nonempty finite linearly ordered subset of $Q$. Then, for every sequence of distinct elements $s_1, \ldots , s_ m \in S \setminus \{ x_0, x_ n \} $, the functor $F^{+}$ carries the inclusion $S \setminus \{ s_1, \ldots , s_ m \} \subseteq S$ (regarded as a $2$-morphism from $S$ to $S \setminus \{ s_1, \ldots , s_ m \} $ in the strict $2$-category $\operatorname{Path}_{(2)}[Q]$) to the $2$-morphism $\gamma _{S, s_1, \ldots , s_ m }$ (regarded as a $2$-morphism from $F(S)$ to $F( S \setminus \{ s_1, \ldots , s_ m \} )$ in the strict $2$-category $\operatorname{\mathcal{C}}$).

It is now clear that the functor $F^{+}$ is unique if it exists: its values on objects, $1$-morphisms, and $2$-morphisms of $\operatorname{Path}_{(2)}[Q]$ are determined by conditions $(0)$, $(1')$, and $(2')$, respectively. To prove existence, it will suffice to show that this prescription is well-defined: namely, that the $2$-morphism $\gamma _{S, s_1, \ldots , s_ m}$ defined above depends only on the sets $S$ and $T = S \setminus \{ s_1, \ldots , s_ m \} $, and not on the order of the sequence $(s_1, \ldots , s_ m )$ (it then follows easily from the construction that the definition of $F^{+}$ on $2$-morphisms is compatible with vertical and horizontal composition). Since the group of all permutations of the set $\{ s_1, \ldots , s_ m \} $ is generated by transpositions of adjacent elements, it will suffice to show that we have

for each $1 \leq i < m$. Replacing $S$ by $S \setminus \{ s_1, \ldots , s_{i-1} \} $, we are reduced to proving that $\gamma _{S, s, t} = \gamma _{ S, t, s }$ whenever $s < t$ are elements of $S - \{ x_0, x_ n \} $. We now distinguish two cases:

• Suppose that the elements $s$ and $t$ are non-consecutive elements of $S$: that is, we have $s = x_ i$ and $t = x_ j$ where $j > i + 1$. In this case, we can identify both $\gamma _{S, s,t}$ and $\gamma _{S, t, s}$ with the horizontal composition

  \[ \operatorname{id}_{ f_{n,n-1} } \circ \cdots \circ \mu _{ x_{j+1}, x_{j}, x_{j-1} } \circ \cdots \circ \mu _{ x_{i+1}, x_ i, x_{i-1} } \circ \cdots \circ \operatorname{id}_{ f_{1,0} }. \]

• Suppose that the elements $s$ and $t$ are consecutive: that is, we have

  \[ S = \{ x_0 < \cdots < r < s < t < u < \cdots < x_ n \} . \]

  In this case, to verify the identity $\gamma _{S, s, t} = \gamma _{S, t, s}$, we can replace $S$ by the subset $\{ r < s < t < u \} $ and thereby reduce to checking the commutativity of the diagram

  \[ \xymatrix@C =80pt@R=50pt{ F( e_{ u, t} ) \circ F( e_{t,s} ) \circ F( e_{s,r} ) \ar@ {=>}[r]^-{ \operatorname{id}_{ F( e_{u,t} )} \circ \mu _{t,s,r} } \ar@ {=>}[d]^-{ \mu _{u,t,s} \circ \operatorname{id}_{ F( e_{s,r})} } & F( e_{u,t} ) \circ F( e_{ t, r} ) \ar@ {=>}[d]^{ \mu _{u,t,r} } \\ F( e_{u,s} ) \circ F( e_{s,r} ) \ar@ {=>}[r]^{ \mu _{ u,s,r} } & F( e_{u,r} ) } \]

  in the category $\underline{\operatorname{Hom}}_{\operatorname{\mathcal{C}}}( F(r), F(u) )$, which is the coherence condition required by the composition contraints for the lax functor $F$ (axiom $(c)$ of Definition 2.2.4.5).