Products in span categories

Proof. For part (1), note that \(C\) has binary coproducts if and only if the diagonal functor \(\Delta \colon C \to C \times C\) admits a left adjoint \(\sqcup \colon C \times C \to C\). The counit of the adjunction is the fold map \(\nabla \colon X \sqcup X \to X\) and the unit is the pair of canonical inclusions \((X \hookrightarrow X \sqcup Y, Y \hookrightarrow X \sqcup Y)\). Conditions (1) to (4) supply the hypotheses of part (2) of Corollary 13.2.4, so this adjunction induces an adjunction \[ \Span _{L,R}(C) \rightleftarrows \Span _{L,R}(C \times C) \simeq \Span _{L,R}(C) \times \Span _{L,R}(C), \] where the adequate triple on \(C \times C\) has classes \(C_L \times C_L\) and \(C_R \times C_R\). Let us spell out the hypotheses of Corollary 13.2.4. The coproduct functor is a morphism of adequate triples by condition (2), while the diagonal functor preserves the relevant classes and pullbacks componentwise. The fold map lies in \(C_L\) by condition (3). Each coprojection, for example \[ X = X \sqcup \emptyset \xrightarrow {\id _X \sqcup (\emptyset \to Y)} X \sqcup Y, \] lies in \(C_L\) by conditions (2) and (3). The naturality square for the fold map is the first pullback square in condition (4). The naturality squares for the coprojections decompose as coproducts of an identity square and the second pullback square in condition (4), so they are pullbacks by condition (2). This proves that the displayed adjunction exists, and hence that \(\Span _{L,R}(C)\) admits binary products. For the terminal object, we similarly regard the initial object \(\emptyset \) of \(C\) as a left adjoint to the functor \(C \to *\). Conditions (3) and (4) allow us to apply Corollary 13.2.4 and obtain an adjunction \(\Span _{L,R}(C) \rightleftarrows \Span (*) \simeq *\) exhibiting \(\emptyset \) as a terminal object of \(\Span _{L,R}(C)\).

It remains to prove the claim about the inclusion \(C_L\catop \hookrightarrow \Span _{L,R}(C)\). The subcategory \(C_L\) admits finite coproducts computed as in \(C\). Indeed, the coprojections lie in \(C_L\) by the preceding argument. Given morphisms \(f\colon X \to Z\) and \(g\colon Y \to Z\) in \(C_L\), their copairing factors as \[ X \sqcup Y \xrightarrow {f \sqcup g} Z \sqcup Z \xrightarrow {\nabla } Z \] and therefore lies in \(C_L\). Conversely, a morphism \(X \sqcup Y \to Z\) in \(C_L\) restricts to morphisms in \(C_L\) because the coprojections lie in \(C_L\). The initial object is initial in \(C_L\) by condition (3). Under the inclusion \(C_L\catop \hookrightarrow \Span _{L,R}(C)\), the resulting product projections are the backwards spans associated with the coprojections, which are precisely the product projections constructed above. Thus this inclusion preserves finite products.

Part (2) is an immediate consequence of (1) using \(\Span _{L,R}(C)\catop \simeq \Span _{R,L}(C)\). For part (3), note first that the initial object \(\emptyset \) in \(C\) becomes both initial and terminal in \(\Span _{L,R}(C)\), and that the zero morphism between objects \(X\) and \(Y\) is given by the span \[ X \leftarrow \emptyset \rightarrow Y. \] Also notice that the coproduct \(X \sqcup Y\) in \(C\) becomes both the product and the coproduct in \(\Span _{L,R}(C)\), via the spans \[ X \sqcup Y \hookleftarrow X \xrightarrow {=} X, \qquad X \sqcup Y \hookleftarrow Y \xrightarrow {=} Y, \qquad X \xleftarrow {=} X \hookrightarrow X \sqcup Y, \qquad Y \xleftarrow {=} Y \hookrightarrow X \sqcup Y. \] It thus remains to compute the four composites and show that they are \(\id _X\), \(0\), \(0\) and \(\id _Y\). The required pullback squares follow from the extensivity assumptions. The first square below is the coproduct of the identity square on \(X\) and the empty pullback square from condition (4) for the morphism \(\emptyset \to Y\), which lies in \(C_R\) by weak coextensivity; the second is obtained symmetrically. The third is the coproduct of the empty pullback square from condition (4) for \(\id _X\) and the identity square on the morphism \(\emptyset \to Y\). Condition (2) guarantees that these coproducts are again pullback squares. Thus we have:

□