Lemma 5.3.8. Consider the wide subcategory \(\Span (\Fin ,\inj ,\all )\) of \(\Span (\Fin )\) whose morphisms are those spans \(S \hookleftarrow U \to T\) for which the left-pointing map is an injection. This is a 1-category, and there is an equivalence of 1-categories \(\Fin _* \simeq \Span (\Fin ,\inj ,\all )\).
Proof. It is clear that \(\Span (\Fin ,\inj ,\all )\) is a 1-category: given two injections \(U \hookrightarrow S\) and \(U' \hookrightarrow S\), if there exists a bijection \(U \iso U'\) over \(S\), then it is unique.
We now construct mutually inverse functors to \(\Fin _*\). Define a functor \[ \Phi \colon \Span (\Fin ,\inj ,\all ) \to \Fin _* \] as follows: on objects, \(\Phi \) sends a finite set \(S\) to \(S_+ = S \sqcup \{*\}\). On morphisms, \(\Phi \) sends a span \(S \hookleftarrow U \to T\) (where the left-pointing map is an injection) to the pointed map \(S_+ \to T_+\) that agrees with \(U \to T\) on \(U\) and sends the complement \(S \setminus U\) (together with the basepoint of \(S_+\)) to the basepoint of \(T_+\).
Conversely, define a functor \[ \Psi \colon \Fin _* \to \Span (\Fin ,\inj ,\all ) \] as follows: on objects, \(\Psi \) sends a finite pointed set \((S,*)\) to \(S \setminus \{*\}\). On morphisms, \(\Psi \) sends a pointed map \(f\colon (S,*) \to (T,*)\) to the span \[ S \setminus \{*\} \hookleftarrow f^{-1}(T \setminus \{*\}) \xrightarrow {f} T \setminus \{*\}, \] where the left-pointing map is the inclusion. One readily verifies that \(\Phi \) and \(\Psi \) are inverse equivalences. □
Generated from the authoritative LaTeX source.