Lemma 17.4.7. Let \[ u\colon \Fin _* \simeq \Span _{\inj ,\all }(\Fin ) \hookrightarrow \Span (\Fin ) \] be the inclusion, and let \(\Rr _*\) and \(\Rr \) denote the forward morphisms in \(\Fin _*\) and \(\Span (\Fin )\), respectively. For every functor \(p\colon E \to \Span (\Fin )\), there is a natural equivalence of functors over \(\Fin _*\) \[ u^*E_{\Rr }(p) \simeq E_{\Rr _*}(u^*p). \]
Proof. By the pullback formula in Construction 17.2.2, it suffices to construct a natural equivalence \[ \Fin _* \times _{\Span (\Fin ),t}\Ar _{\Rr }(\Span (\Fin )) \simeq \Ar _{\Rr _*}(\Fin _*) \] over \(\Fin _*\). The objects on both sides are forward spans, equivalently maps of finite sets \(r\colon I \to J\). A morphism on the left is a commutative square in \(\Span (\Fin )\)
in which \(g\) belongs to \(\Fin _*\). The composite \(gr\) has injective backwards leg because this leg is obtained by pulling back the injective backwards leg of \(g\) along \(r\). Since \(r'\) is forward, the backwards leg of \(r'f\) is the backwards leg of \(f\). The equivalence \(r'f \simeq gr\) therefore shows that \(f\) also belongs to \(\Fin _*\). As \(\Fin _* \hookrightarrow \Span (\Fin )\) is a wide subcategory inclusion, its hom animae are unions of components, so the homotopy making the square commute also lies in \(\Fin _*\). Thus the displayed square is precisely a morphism in \(\Ar _{\Rr _*}(\Fin _*)\), which proves the claim. □
Generated from the authoritative LaTeX source.