Proposition 13.1.11 (Barwick (2017), Proposition 5.6, Haugseng et al. (2023), Theorem 2.1.3). For every adequate triple \((C,C_L,C_R)\) the simplicial anima \(\NSpan _{L,R}(C)\) is a complete Segal anima.

Proof. We start by proving the Segal condition. Let us write \(X := \NSpan _{L,R}(C)\) for ease of notation. For every \(n \geq 0\), consider the subposet \(J_n \subseteq \Tw ^r([n])\) spanned by the objects \((i \leq j)\) with \(j \leq i + 1\):

Commutative diagram generated from the LaTeX source

Note that a functor \(\Tw ^r([n]) \to C\) preserves the pullback squares from Lemma 13.1.8 if and only if it is right Kan extended along the inclusion \(J_n \hookrightarrow \Tw ^r([n])\): if we compute this Kan extension row by row, this follows from the pointwise formula for Kan extensions (Theorem 21.4.3). Concretely, right Kan extension from \(J_n\) fills the diagram by iterated pullbacks, and hence encodes the successive composites of the original string of spans.

We now use the adequacy of \((C,C_L,C_R)\). Starting with a functor \(J_n \to C\) that sends the left-pointing morphisms to \(C_L\) and the right-pointing morphisms to \(C_R\), construct its right Kan extension by induction on \(j-i\). At each step, the value at \((i \leq j)\) is obtained by pulling back the diagram formed by the previously constructed values at \((i \leq j-1)\), \((i+1 \leq j)\) and \((i+1 \leq j-1)\). The adequate-triple axiom guarantees that this pullback exists and that its new left- and right-pointing legs again lie in \(C_L\) and \(C_R\), respectively. Thus restriction to \(J_n\) induces an inclusion of animae \[ X_n = \NSpan _{L,R}(C)_n \hookrightarrow \Map (J_n, C) \] whose image consists precisely of those functors \(J_n \to C\) sending the left-pointing morphisms to \(C_L\) and the right-pointing morphisms to \(C_R\). We now observe that the Segal maps \(e_i\colon [1] \hookrightarrow [n]\) induce inclusions \(\Tw ^r([1]) \hookrightarrow J_n\) which assemble into an equivalence \[ \Tw ^r([1]) \sqcup _{\Tw ^r([0])} \Tw ^r([1]) \sqcup _{\Tw ^r([0])} \dots \sqcup _{\Tw ^r([0])} \Tw ^r([1]) \iso J_n, \] as may be checked directly in posets: the objects \((i \leq i)\) along which we glue are maximal in the adjacent copies of \(\Tw ^r([1])\), so the pushout creates no additional relations. In particular, we get \[ \Map (J_n,C) \iso \Map (\Tw ^r([1]),C) \times _{C^{\simeq }} \Map (\Tw ^r([1]),C) \times _{C^{\simeq }} \dots \times _{C^{\simeq }} \Map (\Tw ^r([1]),C). \] Under this equivalence, the image of the restriction map \(X_n \hookrightarrow \Map (J_n,C)\) corresponds precisely to the target of the Segal map \[ (e_i^*)_{i=1}^n \colon X_n \to X_1 \times _{X_0} \dots \times _{X_0} X_1, \] showing that \(X\) satisfies the Segal condition.

For completeness, first note that the functor \[ C^{\simeq } = X_0 \to X_1 \subseteq \Map (\Tw ^r([1]),C) \] is an inclusion of animae. Indeed, since \(\Tw ^r([1])\) has an initial object we have \(\geom {\Tw ^r([1])} \simeq *\), and thus the constant diagram functor \(C \to \Fun (\Tw ^r([1]),C)\) may be identified with the fully faithful inclusion \(\Fun (\geom {\Tw ^r([1])},C) \hookrightarrow \Fun (\Tw ^r([1]),C)\). It thus remains to show that a span \(X \xleftarrow {l} U \xrightarrow {r} Y\) is an isomorphism in the Segal anima \(\NSpan _{L,R}(C)\) if and only if both \(l\) and \(r\) are isomorphisms in \(C\).

We first show that an invertible span has invertible legs. Let \(Y \xleftarrow {l'} V \xrightarrow {r'} X\) be a left inverse, and let \(Y \xleftarrow {l''} W \xrightarrow {r''} X\) be a right inverse. The two diagrams below exhibit these inverses; pulling them back against each other will produce the isomorphisms needed for a 2-out-of-6 argument. The identities \((l,r) \circ (l',r') = \id \) and \((l'',r'') \circ (l,r) = \id \) are exhibited by commutative diagrams in \(C\) of the following form:

Commutative diagram generated from the LaTeX source
Commutative diagram generated from the LaTeX source

Putting them into one single diagram and forming another pullback, we then obtain:

Commutative diagram generated from the LaTeX source

Since isomorphisms in \(C\) are closed under pullbacks, the maps \(P \to V\) and \(P \to W\) are isomorphisms, so by the 2-out-of-6 property all morphisms along the outer two edges of the diagram are isomorphisms. By the 2-out-of-3 property, then so are the maps \(r'\colon V \to X\) and \(l''\colon W \to Y\), hence by pullback also \(Y \to U\) and \(X \to U\). Finally, another instance of the 2-out-of-3 property shows that \(l\colon U \to X\) and \(r\colon U \to Y\) are isomorphisms. Conversely, if \(l\) and \(r\) are isomorphisms, then the span is isomorphic in \(X_1\) to the identity span on \(U\), and hence lies in the image of \(X_0 \to X_1\). This proves completeness. □

Generated from the authoritative LaTeX source.