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

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?
-

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.

-
 Wow!! It may take me a few more readings- but this absolutely wonderful! Thank you! – Dylan Wilson Feb 15 2011 at 1:52

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!)

-
@David: The representations of those quivers $A_3$ in an $\infty$-category $\mathcal{C}$ are exactly the $2$-simplices of the simplicial set. Also, the thing about representations in spectra is definitely way too advanced for the proof Lurie's thinking of. The idea is that you take the nerve of the poset, show that the pushout exists, then take the new diagram classifying that guy with two new things extended etc. – Harry Gindi Feb 13 2011 at 15:12
In fact, all that the lemma is telling you to do is take iterated pushouts to build up the diagram. – Harry Gindi Feb 13 2011 at 15:15
The relevance of the stated lemma follows from remark 2.7 in the original edition (I assume this will be 1.1.2.7 in the new book or something like that). – Harry Gindi Feb 13 2011 at 15:30
@Harry -- it's all the same argument in different languages. The only point in calling in representations of a quiver is if it rings useful bells, since quiver representations (with whatever coefficients) are basic "atomic" objects in math. In any case the idea is that having a basic diagram in your category implies a whole bunch more, which are conveniently expressed as the stable category those diagrams generate (which you can say in terms of modules over your category, ie functors out of the opposite into the unit, which happens to be spectra). – David Ben-Zvi Feb 13 2011 at 15:37
@David: I'm just saying that it seems almost bound to be circular to derive this straightforward conclusion from the much harder claim regarding categories of spectra and their generators. – Harry Gindi Feb 13 2011 at 16:22
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'.