Let $f:x\to z$ and $g:y\to z$ be morphisms in an $\infty$-category $\mathcal C$. It seems that the square $$\require{AMScd} \begin{CD} \operatorname{Map}_{\mathcal C_{/z}}(f,g) @>>> \operatorname{Map}_{\mathcal C^{\Delta^1}}(f,g)\\ @VVV @VVV \\ \Delta^0 @>{\operatorname{id}_z}>> \operatorname{Map}_{\mathcal C}(z,z) \end{CD}$$ should be (homotopy-)cartesian in the $\infty$-category of spaces. If this is indeed true, does anyone have a reference or a proof?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
2
Let us use the fat slice $\mathcal{C}^{z/}$ (See HTT, $\S$4.2.1) and the model $\operatorname{Hom}_{\mathcal{C}}(x,y)=\operatorname{Fun}(\Delta^1,\mathcal{C})\times _{\mathcal{C}\times \mathcal{C}}\{(x,y)\}$ of the mapping space. By computation, we can check that the square
$$\require{AMScd} \begin{CD} \operatorname{Hom}_{\mathcal{C}^{/z}}(f,g) @>>> \operatorname{Hom}_{\operatorname{Fun}(\Delta^1,\mathcal{C})}(f,g)\\ @VVV @VVV \\ \Delta^0 @>{\operatorname{id}_z}>> \operatorname{Hom}_{\mathcal{C}} (z,z)\end{CD}$$
is cartesian. The right vertical arrow is a Kan fibration, because $\operatorname{ev}_1:\operatorname{Fun}(\Delta^1,\mathcal{C})\to\mathcal{C}$ is an inner fibration. (In general, inner fibrations induce Kan fibrations between various mapping spaces. See, e.g., Lemma 2.4.4.1. The lemma talks about the usual slice, but the proof applies to fat slice as well.) So the above square is homotopy cartesian.
-
$\begingroup$ Thanks so much for this splendid answer. The computation goes like this: let $A,B=\Delta^1$. Then $(\mathcal C^{/z})^{\Delta^1}\cong\mathcal C^{A\times B}\times_{\mathcal C^{A\times\{1\}}}\mathcal C^0$, $\operatorname{Map}_{\mathcal C^{/z}}(f,g)$ is the fiber at $(f,g)$ of $(\mathcal C^{/z})^{\Delta^1}\to\mathcal C^{/z}\times\mathcal C^{/z}$; i.e. of $\mathcal C^{A\times B}\times_{\mathcal C^{A\times\{1\}}}\mathcal C_0\to\mathcal C^{\partial A\times B}$, and this coincides with the fiber of $\mathcal C^{\Delta^1\times\Delta^1}\to\mathcal C^{\sqsupset}$ at $(f,g,\operatorname{id}_z)$. $\endgroup$– TomoCommented Oct 28, 2022 at 2:04
-
$\begingroup$ Here, $\mathcal C^0/\mathcal C_0$ is the discrete simplicial set on the 0-simplices of $\mathcal C$, and $\sqsupset\ \subset\Delta^1\times\Delta^1$ is the simplicial set given by the union of the three morphisms $(0,0)\to(0,1)$, $(1,0)\to(1,1)$, and $(0,1)\to(1,1)$. The fiber of $\mathcal C^{\Delta^1\times\Delta^1}\to\mathcal C^{\sqsupset}$ at $(f,g,\operatorname{id}_z)$ coincides with the fiber of $\operatorname{Map}_{\mathcal C^{\Delta^1}}(f,g)\to\operatorname{Map}_{\mathcal C}(z,z)$ at $\operatorname{id}_z$ as desired. $\endgroup$– TomoCommented Oct 28, 2022 at 2:05