Proof that the homotopy category of a stable $\infty$-category is triangulated

Question

I've been looking at various general strategies for proving that some category is triangulated, and Lurie manages to prove that a huge class of interesting examples of categories that we know about are triangulated in his book Higher Algebra (formerly DAG I-IV and VI).(EDIT: here's a link to the book) The trouble is that I am very new to this language, and so what he calls $\infty$-categorical notions that are basic and easily motivated' I see as foreign and unfamiliar.

The part I'm really interested in is the proof of the octahedral axiom on page 24 of Higher Algebra. He builds a diagram using a proposition from Higher Topos Theory that seems completely out of context (to me!). The proposition says:

``Suppose we are given a diagram of $\infty$-categories $\mathcal{C} \rightarrow \mathcal{D}' \leftarrow \mathcal{D}:p$, where $p$ is a categorical fibration. Let $\mathcal{C}^0$ be a full subcategory of $\mathcal{C}$. Let $\mathcal{K} \subset Map_{\mathcal{D}'}(\mathcal{C}, \mathcal{D})$ be the full subcategory spanned by those functors $F: \mathcal{C} \rightarrow \mathcal{D}$ which are $p$-left Kan extensions of $F\vert\mathcal{C}^0$. Let $\mathcal{K}'\subset \text{Map}_{\mathcal{D}'}(\mathcal{C}^0, \mathcal{D})$ be the full subcategory spanned by those functors $F_0: \mathcal{C}^0 \rightarrow \mathcal{D}$ with the property that, for each object $C \in \mathcal{C}$, the induced diagram $\mathcal{C}^0_{/C} \rightarrow \mathcal{D}$ has a $p$-colimit. Then the restriction functor $\mathcal{K} \rightarrow \mathcal{K}'$ is a trivial fibration of simplicial sets.''

And Lurie says that, in order to prove (TR4), we use this ``repeatedly to construct a map from the nerve of the appropriate partially ordered set into $\mathcal{C}$.'' (See Lurie's book available for download on his webpage.)

Now, obviously this must be some sort of standard use of the proposition, but I would very much like to understand this one proof without reading all of Higher Topos Theory, so we have my question:

1. Is there possibly a more easy-going reference for this proof? or
2. If it doesn't require too much effort, would someone be willing to explain how the cited proposition applies in this instance? or
3. Do I really just have to read Higher Topos Theory up through Chapter 4?

Answer 1

Alright, here's a proof and construction: Suppose we're given a $2$-simplex $X\to Y\to Z$ in $\mathcal{C}$. We have a lemma:

Every $2$-simplex in $\Delta^2\to \mathcal{C}$ can be (right Kan-)extended by zeroes via the map $\Delta^2\hookrightarrow \Delta^1\vee \Delta^3$, which gives diagrams of the form:

$$0\leftarrow X\to Y\to Z\to 0.$$ It is an easy computation to show that right Kan extensions relative to the inclusion of a full and faithful subcategory that is also a sieve are extensions by zero.

Let $\mathfrak{A}\subseteq Fun(\Delta^1\vee \Delta^3,\mathcal{C})$ be the full subcategory spanned by objects whose "first and last" vertices are zero. Then the induced map $\mathfrak{A}\to Fun(\Delta^2, \mathcal{C})$ is a trivial fibration by the theorem.

Then consider the inclusion $$\Delta^1\vee \Delta^3 \cong \Delta^1\times \{0\}\coprod_{\{0\}\times\{0\}} \{0\}\times \Delta^3\hookrightarrow \Delta^1\times \Delta^3$$

Let $\mathfrak{B}$ be the full subcategory of $Fun(\Delta^1\times \Delta^3,\mathcal{C})$ spanned by diagrams that look like the top row in Lurie's diagram. We can now do another right Kan extension by zero.

Things are getting a bit more complicated, so we will consider the diagrams as subcomplexes of $\Delta^2\times \Delta^4$. We may identify our $\Delta^1\times \Delta^3$ with the subcomplex spanned by the set of vertices $P_0:=\{(x,y): x\in \{0,1\}, y\in \{0,1,2\}\}$. Let $P_1=P_0\cup \{(2,1),(1,3)\}$. Let $H$ be the subcomplex of $\Delta^2\times \Delta^4$ spanned by $P_1$. Let $\Delta^1\times \Delta^3\hookrightarrow H$. Taking a right Kan extension, we have extended the diagrams by zero, and then taking the left Kan extension along the inclusion $H\hookrightarrow J$, where $J$ is the subcomplex of $\Delta^2\times \Delta^4$ spanned by the set of vertices $(\Delta^2\times \Delta^4)_0 -\{(2,0), (0,4)\}$, we get a diagram like Lurie's, and also with the property that the canonical map from the category of such diagrams induced by the projection $Fun(\Delta^2\times \Delta^4,\mathcal{C})\to Fun(\{0\}\times \Delta^2,\mathcal{C})$ is a trivial fibration.

Since each stage is built up from cokernels, everything that we claimed exists does exist (the verification is a matter of looking at the definition.) Finally, to deduce that every square is in fact a pushout, we apply the pasting law for pushouts in an $\infty$-category a bunch of times.. With that information in hand, we're done, by Lurie's statement.

Answer 2

I haven't thought through the details, but I believe the rough idea is a simple one, which can be phrased neatly in terms of quiver representations as follows (as I learned from an old lecture of Kontsevich). In the octahedron axiom we're dealing with the basic situation of a pair of composable morphisms. We can think of this as a functor from the $A_3$ quiver, which is a fancy name for the poset made of two composable arrows (and three vertices). This is what you would call a representation of the quiver in your category. So to understand what structure you should expect from having such a representation you first think in the case the target category is say vector spaces. Then it's not hard to see that there are 6 indecomposable objects in the category of quiver representations (they correspond naturally to strictly upper triangular four by four matrices..). Now I think the idea of the proof of the octahedron axiom is that whenever you see a functor from the $A_3$ quiver to your category you can extend it to an exact functor from the stable category the $A_3$ quiver generates (which is representations of its opposite in spectra) - this is where you're using the above proposition from HTT. That means you see in your category not just theoriginal diagram (composition of arrows) but all the diagrams involving the six indecomposables, and thence the octahedron axiom. (Sorry to be vague!)

Answer 3

I did not go through the details, but I think the following happens essentially:

In classical category theory, we have for a functor $\mathcal{C}^0 \to \mathcal{D}$ an essentially unique left Kan extensions to a functor $\mathcal{C}\to \mathcal{D}$ if $\mathcal{D}$ has sufficiently many colimits and $\mathcal{C}^0\subset \mathcal{C}$. Proposition HTT 4.3.2.15 is just the analogue of this in infinity-category language in a relative setting: say that $\mathcal{D} = \mathcal{D}'$ and it has enough colimits, then $\mathcal{K}' = Map(\mathcal{C}^0, \mathcal{D})$ and $\mathcal{K}$ is the simplicial set of left Kan extensions of this. 'Trivial fibration' corresponds to 'essentially unique'.

In the proof of the octahedron axiom, you want to build a diagram, where are many pushouts. The most elegant way to do this, is probably to build it inductively as left Kan extensions.

Answer 4

This point of view is surely somewhat inelegant and rusty, but I think that once it has been polished it exploits only basic definitions: take it as a motivation more than as a proof if you want.

Allow me to start from the beginning recalling that the octahedral axiom (TR4 for short) says that given three distinguished triangles \begin{gather*} X\xrightarrow{f}Y\to Y/X\to X[1] \\ Y\xrightarrow{g}Z\to Z/Y\to Y[1]\\ X\xrightarrow{gf}Z\to Z/X\to X[1] \end{gather*} I can arrange them in the following "braid":

given this, there is a (non-unique) way to complete it with the arrows $s,t$ indicated. This is standard in any book about triangulated categories.

Now, in the $\infty$-categorical setting "distinguished triangles" are replaced by "fiber sequences" like $$ \begin{array}{ccc} A &\to& B &\to& 0 \\ \downarrow && \downarrow && \downarrow\\ 0 &\to& C &\to& A[1] \end{array} $$

Thus, once translated the braid diagram in a stable $\infty$-category $\bf C$ we are in the following situation:

(originally there were colours to help identify different fiber sequences: unfortunately codecogs does not support it!). Axiom TR4 says that we can find arrows $Y/X\to Z/X\to Z/Y$ such that the triangle $Y/X\to Z/X\to Z/Y\to (Y/X)[1]$ is distinguished. This means, at the end of the day, that not only the composite arrow $Z/Y\to Y[1]\to (Y/X)[1]$ can be embedded in a triangle, but also that this embedding can be done "in a coherent way".

Now for the proof.

The completion axiom (which I suppose to hold) implies that the diagram

can be completed with an arrow $Y/X \xrightarrow{\phi} Z/X$ completing the square

Now consider the ojects $V={\rm hocolim}\Big( Y/X \leftarrow{} Y \xrightarrow{g} Z \Big)$ and $W={\rm hocolim}\Big( 0\xleftarrow{} Y/X \xrightarrow{\phi}Z/X \Big)$; arrange them in the diagram

2-out-of-3 now implies that the outer rectangle is a pushout, hence $W\cong Z/Y$. It remains to prove that $V\cong Z/X$; this follows from the 2-out-of-3 property applied to the last diagram: