I’m trying to understand Lurie’s proof that the homotopy category of a stable $\infty$-category is triangulated. In showing TR2, he constructs a diagram
$$\require{AMScd}
\begin{CD}
X @>f>> Y @>>> 0\\
@VVV @VVV @VVV \\
0’ @>>> Z @>>> W \\
@. @VVV @VuVV \\
@. 0’’ @>>> V
\end{CD}$$
in which every square is a pushout in some stable $\infty$-category $\mathcal C$.
He then asserts a map between the suspensions
$$\require{AMScd}
\begin{CD}
X @>>> 0\\
@VVV @VVV \\
0’ @>>> W
\end{CD}$$
$$\require{AMScd}
\begin{CD}
Y @>>> 0\\
@VVV @VVV \\
0’’ @>>> V
\end{CD}$$
giving rise to commutative square
$$\require{AMScd}
\begin{CD}
W @>>> X[1]\\
@VuVV @Vf[1]VV \\
V @>>> Y[1]
\end{CD}$$
in $h\mathcal C$. I think in fact what is needed for this commutative square is that the above map between suspensions specifically have components $f$ and $u$ between the initial vertices and terminal vertices, respectively.
By repeated application of HTT.4.3.2.15, the first (large) diagram is determined up to contractible choices by $f$, and, if $\mathcal C$ is stable, also determined up to contractible choices by $u$. Similarly, the map of suspensions is determined by the map $X\to Y$ or by the map $X[1]\simeq W\to V\simeq Y[1]$ (as $\Sigma$ is an equivalence). So the data of the large diagram is equivalent to the data of a map between the suspensions, and each is specified two different ways (via $f$/the map on initial vertices or $u$/the map on cocone points). I want to know why these are in correspondence. Another way of saying this is, the map $f$ determines, via the large diagram, a map $u$, which determines a map $X[1]\to Y[1]$ (always up to contractible choices), but why is this map homotopic to $f[1]$? This is equivalent to the assertion that the construction of the large diagram computes the suspension functor $\Sigma$ on edges of $\mathcal C$. One way to see this would be to construct a map between suspensions (a diagram $\Delta^1\times\Delta^1\times\Delta^1\to\mathcal C$) directly from the data of the large diagram, but I don’t see how to fill in the most obvious candidate. (I could do so if I knew how to fill an outer horn $\Delta^3_0\hookrightarrow\mathcal C$ with the property that both interior vertices are zero objects, so every edge is a zero map.) Any tips would be a big help – thank you!
Edit 5/20
I can see the claim if it is true that given a cofiber sequence $X\to Y\to Z$ corresponding to a pushout
$$\require{AMScd}
\begin{CD}
X @>>> Y\\
@VVV @VVV \\
0 @>>> Z,
\end{CD}$$
then if I replace the bottom 2-simplex ($X\to 0\to Z$) of the diagram $\Delta^1\times\Delta^1\to\mathcal C$ with any other one with the same vertices and long edge, the resulting diagram $\Delta^1\times\Delta^1\to\mathcal C$ is still a pushout.
Best Answer
"This is equivalent to the assertion that the construction of the large diagram computes the suspension functor $\Sigma$"
My previous answer was based on me misreading this quote :)
You want to show that this large diagram computes $\Sigma$. Lurie says some words about why that is : he says that the large diagram induces a morphism from one square to the next, namely from the square
\begin{CD}X @>>> 0 \\ @VVV @VVV \\ 0 @>>> W\end{CD} to the square \begin{CD}Y @>>> 0 \\ @VVV @VVV \\ 0 @>>> V\end{CD}
Now the first square (the second too, but I need it for the first) is left Kan extended from its restriction to the span $0\leftarrow X \to 0$ (that is what it means to be a pushout), so a map between these two squares is entirely determined by a map between the corresponding spans.
But now the second span (the first one too, but I need it for the second) is right Kan extended from the single vertex $Y$, so a map between the spans is the same thing as a map between these vertices. In this case, by design, the map between the vertices is $f$.
What I'm saying is : the map between the squares that you get from the large diagram, which one $W\to V$ is precisely your $u$ , is the only map (up to a contractible space) of squares which restricts to $f : X\to Y$. But the map of squares which induces $\Sigma f : \Sigma X\to \Sigma Y$ also restricts to $f$, by definition.
So the two maps of squares must be the same, and in particular the two maps $u$ and $\Sigma f: \Sigma X\to \Sigma Y$ must be the same.
So this reduces to showing that the two squares
(\begin{CD}X @>>> 0 \\ @VVV @VVV \\ 0 @>>> W\end{CD} and the other one with $Y$)
are indeed pushout squares. But for both it follows from pasting of pushout squares.
EDIT : Regarding the comments. If you agree that the indexing category for the big diagram is a poset, then a map of squares in this diagram (i.e. a map $(\Delta^1)^3\to K$ where $K$ is the indexing category) is entirely determined by where it sends the vertices, together with the property that for each arrow in $(\Delta^1)^3$, the corresponding vertices in $K$ have an arrow between them.
So here, to get an arrow between the two squares in question from the big diagram, you need an arrow from $X$ to $Y$ (ok you have one, it's $f$), an arrow from $0$ to itself (ok, it's $id$), an arrow from $0'$ to $0''$ (ok, just go $0' \to Z\to 0''$), and finally an arrow from $W$ to $V$ (ok, it's $u$). Crucially, these arrows are in $K$, so you get a map $(\Delta^1)^3\to K$ (again, here I'm really using that $K$ is a poset) and thus, because your big diagram was originally something like $K\to \mathcal C$, you can precompose and get $(\Delta^1)^3\to \mathcal C$. Because of how you chose the vertices and arrows, this map of squares has, on the top left vertex $f$ and on the bottom right vertex $u$, therefore $u$ is identified with $\Sigma f$.
(note : I said that I used that $K$ was a poset, but in fact if $K$ were only a $1$-category, all hope would not have been lost, as we would simply have had to further check that some diagrams commute - in a poset, any diagram commutes so we can skip this step).
(another way to phrase this is that (nerves of) posets are $1$-coskeletal )
EDIT 2 : I was a bit quick when I said $K$ is a poset. I meant that the $\infty$-category presented by $K$ was a poset, i.e. that $K$ was categorically equivalent to a poset. You can see this by computing $\mathfrak C[K]$, which you can do by explicitly writing $K= (\Delta^1)^2\coprod_{\Delta^1}(\Delta^1)^2\coprod_{\Delta^1}(\Delta^1)^2$ (which you can easily simplify, up to categorical equivalence to $(\Delta^1\times \Delta^2)\coprod_{\Delta^{\{1\}}\times\Delta^{\{1,2\}}} (\Delta^1 \times \Delta^1)$, and then you have to do a bit of work)