3
$\begingroup$

In Lurie's "Higher topos theory" lemma 4.3.2.7, I’m trying to understand “In particular, we may identify $p$-colimits of $F$ with $p$-colimits of $F_0$”:

Lemma 4.3.2.7. Suppose we are given a diagram of $\infty$-categories \xymatrix{ \calC^{0} \ar@{^{(}->}[d] \ar[r]^{F_0} & \calD \ar[d]^{p} \ \calC \ar[r] \ar[ur]^{F} & \calD' }

as in Definition 4.3.2.2, where $p$ is a categorical fibration and $F$ is a $p$-left Kan extension of $F_0$. Then the induced map $$\mathcal D_{F/} \to \mathcal D'_{p F/} \times_{\mathcal D'_{p F_0/}} \mathcal D_{F_0/}$$ is a trivial fibration of simplicial sets. In particular, we may identify $p$-colimits of $F$ with $p$-colimits of $F_0$.

It seems that here we have $C\rightarrow C*\mathrm{pt}$ is a homotopy pushout of right cone $C_0\rightarrow C_0*\mathrm{pt}$ via the embedding of quasi-categories $C_0\rightarrow C$, but why?

Or, is there another way to figure out “In particular, we may identify $p$-colimits of $F$ with $p$-colimits of $F_0$.”?

Improve this question
$\endgroup$
1
  • 2
    $\begingroup$ Another version of the second half of this statement is given in Kerodon. It's a bit more explicit: kerodon.net/tag/030V $\endgroup$
    – daniel gratzer
    Commented Jun 13, 2022 at 7:38

1 Answer 1

Reset to default
2
$\begingroup$

Let me answer first the question about the homotopy pushout. It is in general not the case. Consider for instance the inclusion $\Delta^0 \to \Delta^1$. Then $\Delta^0 \star * = \Delta^1$ so that the homotopy pushout with $\Delta^1$ along $\Delta^0$ (computed as sinply the pushout, because it's along a cofibration) is just $\Lambda^2_0$, which is already a quasicategory, whereas $\Delta^1\star * = \Delta^2$, and they are not equivalent.

For the question about this comment, note that you can reformulate the statement of the lemma as : the following square is a pullback square :

$\require{AMScd} \begin{CD}D_{F/} @>>> D_{F_0/} \\ @VVV @VVV \\ D'_{pF/} @>>> D'_{pF_0/} \end{CD}$

Now in this kind of situation, a diagram in the top left hand corner which is $p$-initial when moved to the right was $p$-initial to begin with. This is 4.3.1.5.(4) in HTT.

This shows that a cocone under $F$ wich restricts to a $p$-colimit of $F_0$ is a $p$-colimit of $F$. See Daniel's comment below to see why there shouldn't be a converse in general.

Given a $p$-colimit of $F_0$, say $\overline{F_0}: C_0^\triangleright \to D$, by relative Kan extension, if you're also given an extension $\overline F : C^\triangleright \to D'$ of $p\circ \overline{F_0}$, then you get a diagram $\Delta^0\to D_{F/}$ which becomes a $p$-colimit of $F_0$ under restriction, so again by the above, a $p$-colimit of $F$.

Improve this answer
$\endgroup$
13
  • 1
    $\begingroup$ Could you elaborate slightly on "Kan extension gives you something with a map from F"? I'm unsure how to do this since we only have a relative Kan extension, so it seems non-obvious that one can lift something from $D_{F_0/}$ to $D_{F/}$ without something from $D'_{pF/}$ or similar. $\endgroup$
    – daniel gratzer
    Commented Jun 13, 2022 at 9:29
  • $\begingroup$ @DanielGratzer : Yes, that's probably right... I went a bit too quick there. This means one probably needs to read the statement as a one-directional thing : "$p$-colimits of $F$ are $p$-colimits of $F_0$ (but not necessarily conversely)" $\endgroup$
    – Maxime Ramzi
    Commented Jun 13, 2022 at 9:33
  • 1
    $\begingroup$ @DanielGratzer : This iff is correct, because you start with a diagram $\overline F$, in other words you have something in $D'_{pF/}$ $\endgroup$
    – Maxime Ramzi
    Commented Jun 13, 2022 at 9:37
  • 1
    $\begingroup$ And you see that the Kerodon statement is less vague than the one in HTT :) $\endgroup$
    – Maxime Ramzi
    Commented Jun 13, 2022 at 9:38
  • 1
    $\begingroup$ @DanielGratzer I tried to give it a shot, let me know if my answer is clear :) $\endgroup$
    – Maxime Ramzi
    Commented Jun 13, 2022 at 11:28

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .