Proposition 19.7.9. The construction of Definition 19.7.8 defines a functor \[ \Vect (-)^{\simeq }\colon \Top \catop \longrightarrow \CRig (\An ). \] Its underlying anima is computed by the same colimit in \(\An \). If \(X\) is paracompact Hausdorff, the inclusion of the zeroth simplicial degree induces a natural bijection \[ \pi _0\Vect ^{\disc }(X)^{\simeq } \xrightarrow {\cong } \pi _0\Vect (X)^{\simeq }. \]

Proof. Functoriality follows from pullback. The \(\infty \)-category \(\simp \catop \) is sifted by Proposition 21.6.9, and the forgetful functors \[ \CRig (\An )\longrightarrow \CMon (\An )\longrightarrow \An \] create sifted colimits. For the second functor, this follows by regarding \(\CMon (\An )\) as the full subcategory of \(\Fun (\Span (\Fin ),\An )\) spanned by the finite-product-preserving functors: pointwise sifted colimits preserve this condition by Lemma 21.6.11. For the first functor, use \(\CRig (\An )=\CAlg (\CMon (\An ))\), the fact that \(\CMon (\An )\) is presentably symmetric monoidal by Theorem 18.5.3, and [Lurie (2017), Corollary 3.2.3.2]. This proves the assertion about the underlying anima.

It remains to identify its path components. Applying \(\pi _0\) to the geometric realization gives the coequalizer of the two maps from simplicial degree \(1\) to degree \(0\). Every vector bundle over \(X\times \abs {\Delta ^n}\) is isomorphic to the pullback of its restriction to a vertex: the product \(X\times \abs {\Delta ^n}\) is again paracompact Hausdorff, and the identity is homotopic to the composite of the projection with the inclusion of a vertex, so this follows from Theorem 9.1.4. In particular, degree \(0\) surjects onto the coequalizer. The two endpoint restrictions of a vector bundle over \(X\times [0,1]\) are isomorphic by the same theorem, so the two maps in the coequalizer agree. The coequalizer is therefore \(\pi _0\Vect ^{\disc }(X)^{\simeq }\). □

Generated from the authoritative LaTeX source.