Geometric realizations

Proof. Using that \(\Iso (X) \simeq \Fun ([1],X)\), we obtain by Proposition 3.3.4 equivalences \[ \Fun ^{\Map ([1],X)}(X,D) \simeq \Fun ^{\Iso (X)^{\simeq }}(X,D) \simeq \Fun (X,D), \] which shows that the identity map \(X \to X\) exhibits \(X\) as a localization of \(X\) at all its morphisms. This gives the claim. □

Proof. We may simply compose the equivalence \(\Fun (\geom {C},\Gamma ) \iso \Fun ^{\Map ([1],C)}(C,\Gamma )\) with the equivalence \(\Fun ^{\Map ([1],C)}(C,\Gamma ) \iso \Fun (C,\Gamma )\) from Lemma 3.3.3. □

Proof. We start by showing that (1) implies (2). By (1), the category \(\geom {[1]}\) is a groupoid, so it suffices by Proposition 1.4.11 to show that for every groupoid \(\Gamma \) the induced map \[ \Map (*,\Gamma ) \to \Map (\geom {[1]},\Gamma ) \] is an equivalence. By Lemma 3.4.3, this map corresponds under the canonical equivalences to the map \[ p_{[1]}^*\colon \Gamma \to \Map ([1],\Gamma ). \] But this map is an equivalence since \(\Gamma \) is a groupoid, finishing the proof.

For (2) \(\implies \) (3), the equivalence \(\geom {[1]}\iso *\) and the universal property of geometric realization show that precomposition with \(p_{[1]}\colon [1]\to *\) induces an equivalence \[ C \iso \Fun ^{\Map ([1],[1])}([1],C), \] where the right-hand side is a full subcategory of \(\Fun ([1],C)\) by construction. Thus \(p_{[1]}^*\) exhibits \(C\) as that full subcategory.

The Rezk equivalence \(C\iso \Iso (C)\) identifies \(p_{[1]}^*\) with the composite \(C\to \Iso (C)\xrightarrow {\pi _{\Iso }}\Fun ([1],C)\). Hence (3) and (4) are equivalent.

For (3) \(\implies \) (5), recall that \(C\) is a groupoid if and only if the map \(C \to \Fun ([1],C)\) is an equivalence. Since this functor is a full subcategory by (3), it follows from Lemma 3.2.12 that we may check this on objects, giving the criterion from (5).

We will now deduce (6) from (5). To show \(\lra {\Iso (C)^{\simeq }}_C\) is a groupoid, it suffices by (5) to show that the map \((\lra {\Iso (C)^{\simeq }}_C)^{\simeq } \to \Map ([1],\lra {\Iso (C)^{\simeq }}_C)\) is an equivalence. To this end, consider the following commutative diagram, where the two horizontal maps are induced by the inclusion \(i\colon \lra {\Iso (C)^{\simeq }}_C \hookrightarrow C\):

By the 2-out-of-3 property it remains to show that the top map is an equivalence. To construct an inverse, we consider the inclusion \(\imath _C\colon C^{\simeq } \to C\). It sends all morphisms to isomorphisms, so induces a functor \(C^{\simeq } \to \lra {\Iso (C)^{\simeq }}_C\). Since the source is a groupoid, it factors through a map \(\varphi \colon C^{\simeq } \to (\lra {\Iso (C)^{\simeq }}_C)^{\simeq }\). To check the relations \(\varphi \circ i^{\simeq } = \id \) and \(i^{\simeq } \circ \varphi = \id \), we may do so after composing with the embedding \(\imath _C\colon C^{\simeq } \hookrightarrow C\) from Corollary 2.5.3 and the embeddings \((\lra {\Iso (C)^{\simeq }}_C)^{\simeq } \hookrightarrow \lra {\Iso (C)^{\simeq }}_C\) and \(\lra {\Iso (C)^{\simeq }}_C \hookrightarrow C\) (Lemma 3.1.5) after which the claim becomes a tautology. This establishes (6).

Assume (6). The functor \(C^{\simeq } \to \lra {\Iso (C)^{\simeq }}_C\) constructed above is then a functor between groupoids. Its map on groupoid cores is inverse to the equivalence \(i^{\simeq }\) constructed in the preceding paragraph. Since the groupoid-core inclusions of its source and target are equivalences by Axiom G and Proposition 1.4.15, the functor itself is an equivalence by 2-out-of-3. This proves (7).

Finally, we show that (7) implies (1). The localization functor \(\lambda _C\colon C \to \geom {C}\) sends all morphisms of \(C\) to isomorphisms, hence it factors through the subcategory of \(\geom {C}\) spanned by its isomorphisms. By (7) this subcategory is equivalent to the groupoid core of \(\geom {C}\). The resulting functor \(C \to \geom {C}^{\simeq }\) still inverts all morphisms in \(C\), hence induces a functor \(\geom {C} \to \geom {C}^{\simeq }\). By uniqueness of the localization factorization, the composite \(\geom {C} \to \geom {C}^{\simeq } \hookrightarrow \geom {C}\) is identified with the identity. Thus the embedding \(\geom {C}^{\simeq } \hookrightarrow \geom {C}\) admits a section and is an equivalence by Lemma 1.6.24. It follows that \(\geom {C}\) is a groupoid. □

Proof. It will suffice to show that the map \(\geom {[1]} \to *\) is an equivalence. By Proposition 1.4.11, it will suffice to show that for any category \(D\), the induced functor \(D^{\simeq } \simeq \Map (*,D) \to \Map (\geom {[1]},D) \simeq \Map ^{\Map ([1],[1])}([1],D)\) is an equivalence. Recall from Remark 2.1.29 that the groupoid \(\Map ([1],[1])\) is a disjoint union of three points, corresponding to the identity on \(0\), the identity on \(1\), and the canonical map from \(0\) to \(1\) in \([1]\). Spelling out the definition of \(\Map ^{\Map ([1],[1])}([1],D)\), we obtain a pullback square

The bottom map is the third power of the embedding \(p_{[1]}^*\colon D^{\simeq }\to \Map ([1],D)\). Hence the pullback consists of those morphisms \(f\colon x\to y\) for which \(\id _x\), \(\id _y\), and \(f\) lie in the image of \(p_{[1]}^*\). The first two conditions are automatic, while the third says precisely that \(f\) is an isomorphism. The Rezk equivalence \(D^{\simeq }\iso \Iso (D)^{\simeq }\) therefore identifies the pullback with \(D^{\simeq }\), compatibly with the displayed map from \(D^{\simeq }\). This proves the claim. □

Proof. By Propositions 3.4.4 and 3.4.5, the functor \(\Iso (D)\to \Fun ([1],D)\) is a full subcategory. Unwinding, this means we have a pullback square

The transformation \(\alpha \) determines a term of the upper right corner, and the right-hand map restricts it to its components. If every component is invertible, applying this hypothesis to the universal object in the anima \(C^{\simeq }\) gives a lift to the lower left corner. The pullback property then supplies a lift \(C\to \Iso (D)\) of the functor encoding \(\alpha \). It follows from Lemma 1.7.11 that \(\Fun (C,\Iso (D)) \simeq \Iso (\Fun (C,D))\), so that this lift provides the inverse data for \(\alpha \) in \(\Fun (C,D)\), showing that \(\alpha \) is a natural isomorphism. Conversely, evaluation at each object sends an inverse of \(\alpha \) to an inverse of its component. □

Proof. By Definition 1.8.1, it will suffice to show that the square becomes a pullback square after applying \(\Map (-,E)\) for every category \(E\). By Corollary 1.4.13 and Lemma 3.4.3, there are equivalences \[ \Map (\geom {C},E) \simeq \Map (\geom {C},E^{\simeq }) \simeq \Map (C,E^{\simeq }), \] and similarly for \(C\) replaced with \(C'\), \(D\) and \(D'\). The claim now follows from the assumption on the original square. □