Category of isomorphisms is equivalent to underlying $\infty$-category

Question

Let $\mathscr{C}$ be an $\infty$-category (for example taking quasicategories as a model). Recall that the arrow category is $\mathsf{Ar}(\mathscr{C}) = \mathsf{Fun}([1], \mathscr{C})$. We denote by $\mathsf{Isom}(\mathscr{C})$ the full sub-$\infty$-category spanned by the equivalences. Then, there is the expected result that $\mathsf{Isom}(\mathscr{C}) \simeq \mathscr{C}$.

This follows for example from Kerodon 02BY where Lurie even shows that $\mathrm{ev}_0, \mathrm{ev}_1 : \mathsf{Isom}(\mathscr{C}) \to \mathscr{C}$ are trivial fibrations.

However, the proof there is taken as the corollary of a much more general technical-looking result. It feels like that's overkill for this situation which is why I'm looking for a more immediate way. If one tried to prove this $1$-categorically, then one could write down inverse functors and explicit natural isomorphisms realizing that the functors realize equivalences of categories. But I couldn't manage to transport such a technique to $\infty$-categories.

Question. How do you prove $\mathsf{Isom}(\mathscr{C}) \simeq \mathscr{C}$ if you may assume standard results from $\infty$-category theory? Arguing "model-independently" is preferred but I would also be interested in seeing a direct quasicategorical proof (without going through all that trouble as in Kerodon.)

I'll admit I didn't read the argument in Kerodon, so possibly one could adapt the situation there and extract an easier proof.

Answer 1

$\newcommand{\Hom}{\operatorname{Hom}}$If you know how to compute mapping anima in arrow categories, there is an easy model-independent proof: Recall that for morphisms $f\colon x\to y$ and $g\colon a\to b$ in $\mathcal C$, we have $$ \Hom_{\operatorname{Ar}(\mathcal C)}(f,g) = \Hom_{\mathcal C}(x,a) \times_{\Hom_{\mathcal C}(x,b)} \Hom_{\mathcal C}(y,b). $$ It is now straightforward that the functor $$ \alpha\colon \mathcal C \to \operatorname{Isom}(\mathcal C),\quad c\mapsto \mathrm{id}_c $$ is fully faithful. The essential image coincides with $\operatorname{Isom}(\mathcal C)$: if $f\colon x\to y$ is an isomorphism, then the commutative square $$ \require{AmsCD} \begin{CD} x @>{\mathrm{id}_x}>> x \\ @V{\mathrm{id}x}VV @VV{f}V \\ x @>>{f}> y \end{CD} $$ shows that $\mathrm{id}_x \simeq f$ in $\operatorname{Isom}(\mathcal C)$. Hence, $\alpha$ is an equivalence of $\infty$-categories.

Now, note that $\mathrm{ev}_0\circ \alpha = \mathrm{ev}_1\circ\alpha = \mathrm{id}_{\mathcal C}$, hence $\mathrm{ev}_0$ and $\mathrm{ev}_1$ are also equivalences of $\infty$-categories.

Answer 2

I was actually thinking recently about something quite similar. You can argue model-independently as follows, as long as you assume you have established some facts about $\infty$-category theory. It is possible that Lurie's treatment of the material does not cover some of this stuff before this point in Kerodon (it is quite likely in fact), but I think you should in principle be able to establish all this before you start asking yourself your question.

I will prove the statement for $\mathrm{ev}_0$. The other case follows by a similar argument. The inclusion $i\colon[0]\to[1],0\mapsto 0$ and the projection $p\colon[1]\to[0]$ give us a factorization $\mathcal{C}\xrightarrow{p^*}\mathsf{Fun}([1],\mathcal{C})\xrightarrow{i^*}\mathcal{C}$ of the identity functor on $\mathcal{C}$. Since $\mathsf{Isom}(\mathcal{C})$ is the essential image of $p^*$ (in quasicategories, you can see this from the homotopy equivalence $\Delta^0\simeq NE(2)$, in which $E(2)$ is the groupoid on two objects with unique isomorphisms between any two objects; the fact that this is a homotopy equivalence rather than just a general weak equivalence means you can prove $\mathsf{Fun}(-,\mathcal{C})$ preserves this homotopy equivalence quite easily, so no advanced theory is needed here). By the $2$-out-of-$3$ property of equivalences of $\infty$-categories, it thus suffices to show that $p^*\colon\mathcal{C}\to\mathsf{Isom}(\mathcal{C})$ is an equivalence. Since this functor is essentially surjective, to do this, it suffices to show that the morphism $p^*\colon\mathcal{C}\to\mathsf{Fun}([1],\mathcal{C})$ is fully faithful.

As an intermezzo, note that if $K$ is an $\infty$-groupoid, we have $K\simeq\mathsf{Ar}(K)$. This follows from the fact that $[1]$ is weakly contractible. In full model-independent glory, for this you probably need the adjunction $|-|\colon\mathsf{Cat}_\infty\rightleftarrows\mathsf{An}\colon\mathrm{incl}$, where $|-|$ is localization at all morphisms. But in all models I know, it just follows quite easily, so pick your poison. So in particular, if $K$ is an $\infty$-groupoid, then $K\to\mathsf{Isom}(K)$ is an equivalence of $\infty$-categories. There is another way to show this equivalence, see the appendix below; it still relies on some nontrivial background about $\infty$-categories.

Back to the main show. We want to show that the map $\mathcal{C}(x,y)\to\mathsf{Isom}(\mathcal{C})(\mathrm{id}_x,\mathrm{id}_y)\simeq\mathsf{Ar}(\mathcal{C})(\mathrm{id}_x,\mathrm{id}_y)$ induced by $p^*$ is an equivalence. By our intermezzo, it suffices to show that $\mathsf{Ar}(\mathcal{C}(x,y))\simeq\mathsf{Ar}(\mathcal{C})(\mathrm{id}_x,\mathrm{id}_y)$, via the the map induced by ''transposition of the square''. This is the map $[1]\times[1]$ which flips the two copies of $[1]$. This can be checked by looking at the pullback square which defines mapping anima, and using that $\mathsf{Fun}([1],-)$ preserves pullbacks in $\mathsf{Cat}_\infty$. More precisely, all vertical morphisms in the commutative diagram $$\require{AMScd}\begin{CD} *@>{(\mathrm{id}_x,\mathrm{id}_y)}>>\mathsf{Fun}([1]\times\{0,1\},\mathcal{C}) @<{\mathrm{restr}}<<\mathsf{Fun}([1]\times[1],\mathcal{C})\\ @V{\mathrm{id}}VV @VV{\mathrm{flip}}V @VV{\mathrm{flip}}V\\ * @>{(\mathrm{id}_x,\mathrm{id}_y)}>>\mathsf{Fun}(\{0,1\},\mathsf{Ar}(\mathcal{C}))@<{\mathrm{restr}}<<\mathsf{Fun}([1],\mathsf{Ar}(\mathcal{C})) \end{CD}$$ are equivalences, and the pullbacks of the rows give you both sides of the required equivalence.

Appendix. In order to show that $p^*\colon K\to\mathsf{Isom}(K)$ is an equivalence, it suffices to show that it is $(-1)$-truncated in $\mathsf{Cat}_\infty$ (if we say it suffices to show it is an equivalence in $\mathsf{An}$, we cannot really proceed since $\mathsf{Isom}(K)$ is defined in terms of the category $[1]$), since we already know it is essentially surjective. We use here that $\mathsf{Cat}_\infty(A,B)\simeq\mathsf{Fun}(A,B)^{\simeq}$, so that $(-1)$-truncated functors in $\mathsf{Cat}_\infty$ between $\infty$-groupoids are actually fully faithful functors.

All in all, we want to show that the commutative square $$\require{AMScd}\begin{CD} \mathsf{Fun}([0],K)@>{\mathrm{id}}>>\mathsf{Fun}([0],K)\\ @V{\mathrm{id}}VV @VV{p^*}V\\ \mathsf{Fun}([0],K)@>>{p^*}>\mathsf{Fun}([1],K) \end{CD}$$ in $\mathsf{Cat}_\infty$ is a pullback square. Since $\mathsf{Fun}(-,K)$ sends pushouts in $\mathsf{Cat}_\infty$ to pullbacks in $\mathsf{Cat}_\infty$, it suffices to show that the square $$\require{AMScd}\begin{CD} [1] @>{p}>> [0]\\ @V{p}VV @VV{\mathrm{id}}V\\ [0]@>>{\mathrm{id}}> [0] \end{CD}$$ is a pushout in $\mathsf{Cat}_\infty$. This is stating that $[1]\to[0]$ is an epimorphism in $\mathsf{Cat}_\infty$, which sounds believable, but let us actually prove it. You can argue directly, but I will only sketch the argument since it is a bit tedious. After that, I will give two quicker proofs, that do require more background knowledge.

Given an $\infty$-category $\mathcal{E}$, a commutative diagram $$\require{AMScd}\begin{CD} [1] @>{p}>> [0]\\ @V{p}VV @VV{y}V\\ [0]@>>{x}> \mathcal{E} \end{CD}$$ in $\mathsf{Cat}_\infty$ is the data of two objects $x,y\in\mathcal{E}$ and a morphism $f$ in $\mathcal{E}$ (corresponding to the map $[1]\to\mathcal{E}$) that is both an identity morphism on $x$ and an identity morphism on $y$ (I mean this in a very homotopy-invariant sense, so up to homotopy that may change the source and target objects, $f$ is such an identity morphism). It follows that we can find a map $z\colon[0]\to\mathcal{E}$ together with homotopies $x\simeq z$ and $z\simeq y$ in $\mathcal{E}$. This proves that the object $[0]$ (together with the identity functors on it) in the right bottom corner of the second square above satisfies a truncated version of the universal property of the pushout in $\mathsf{Cat}_\infty$. All categories in that square are so simple that it is likely you don't need to work harder to establish all the higher coherences involved in the universal properties.

If you want to argue quicker, you can for instance note that the diagram will (sort of by the standard model for the latter) model the localization of the $\infty$-category $[0]$ at the identity morphism on $0$. This is just $[0]$ again.

You can also invoke straightening-unstraightening and just compute the pushout in $\mathsf{Cat}_\infty$ in terms of the cocartesian fibration associated to the diagram. In our case, this is just the Grothendieck opfibration of $1$-categories, and a quick argument gives the desired result.