Proof.
Say RF is defined at X, Y with values A, B. Let RF(f) : A \to B be the induced morphism, see Lemma 13.14.3. We may choose a distinguished triangle (A, B, C, RF(f), b, c) in \mathcal{D}'. We claim that C is a value of RF at Z.
To see this pick s : X \to X' in S such that there exists a morphism \alpha : A \to F(X') as in Categories, Definition 4.22.1. We may choose a commutative diagram
\xymatrix{ X \ar[d]_ f \ar[r]_ s & X' \ar[d]^{f'} \\ Y \ar[r]^{s'} & Y' }
with s' \in S by MS2. Using that Y/S is filtered we can (after replacing s' by some s'' : Y \to Y'' in S) assume that there exists a morphism \beta : B \to F(Y') as in Categories, Definition 4.22.1. Picture
\xymatrix{ A \ar[d]_{RF(f)} \ar[r]_-\alpha & F(X') \ar[r] \ar[d]^{F(f')} & A \ar[d]^{RF(f)} \\ B \ar[r]^-\beta & F(Y') \ar[r] & B }
It may not be true that the left square commutes, but the outer and right squares commute. The assumption that the ind-object \{ F(Y')\} _{s' : Y' \to Y} is essentially constant means that there exists a s'' : Y \to Y'' in S and a morphism h : Y' \to Y'' such that s'' = h \circ s' and such that F(h) equal to F(Y') \to B \to F(Y') \to F(Y''). Hence after replacing Y' by Y'' and \beta by F(h) \circ \beta the diagram will commute (by direct computation with arrows).
Using MS6 choose a morphism of triangles
(s, s', s'') : (X, Y, Z, f, g, h) \longrightarrow (X', Y', Z', f', g', h')
with s'' \in S. By TR3 choose a morphism of triangles
(\alpha , \beta , \gamma ) : (A, B, C, RF(f), b, c) \longrightarrow (F(X'), F(Y'), F(Z'), F(f'), F(g'), F(h'))
By Lemma 13.14.4 it suffices to prove that RF(Z') is defined and that the arrow \gamma : C \to F(Z') induces an isomorphism C \to RF(Z'). Namely, then we will get an isomorphism
(A, B, C, RF(f), b, c) \longrightarrow (RF(X'), RF(Y'), RF(Z'), RF(f'), RF(g'), RF(h'))
of triangles and by TR1 we conclude that the target is a distinguished triangle. Consider the category \mathcal{I} of Lemma 13.5.10 of triangles
\mathcal{I} = \{ (t, t', t'') : (X', Y', Z', f', g', h') \to (X'', Y'', Z'', f'', g'', h'') \mid (t, t', t'') \in S\}
To show that the system F(Z'') is essentially constant over the category Z'/S is equivalent to showing that the system of F(Z'') is essentially constant over \mathcal{I} because \mathcal{I} \to Z'/S is cofinal, see Categories, Lemma 4.22.11 (cofinality is proven in Lemma 13.5.10). For any object W in \mathcal{D}' we consider the diagram
\xymatrix{ \mathop{\mathrm{colim}}\nolimits _\mathcal {I} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, F(X'')) & \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, A) \ar[l] \\ \mathop{\mathrm{colim}}\nolimits _\mathcal {I} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, F(Y'')) \ar[u] & \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, B) \ar[u] \ar[l] \\ \mathop{\mathrm{colim}}\nolimits _\mathcal {I} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, F(Z'')) \ar[u] & \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, C) \ar[u] \ar[l] \\ \mathop{\mathrm{colim}}\nolimits _\mathcal {I} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, F(X''[1])) \ar[u] & \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, A[1]) \ar[u] \ar[l] \\ \mathop{\mathrm{colim}}\nolimits _\mathcal {I} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, F(Y''[1])) \ar[u] & \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, B[1]) \ar[u] \ar[l] }
where the horizontal arrows are given by composing with (\alpha , \beta , \gamma ). Since filtered colimits are exact (Algebra, Lemma 10.8.8) the left column is an exact sequence. Thus the 5 lemma (Homology, Lemma 12.5.20) tells us the map
\mathop{\mathrm{colim}}\nolimits _\mathcal {I} \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, F(Z'')) \longrightarrow \mathop{\mathrm{Mor}}\nolimits _{\mathcal{D}'}(W, C)
is bijective. We conclude that F(Z'') is essentially constant over \mathcal{I} with value C by part (4) of Categories, Lemma 4.22.9.
\square
Comments (5)
Comment #556 by Nuno on
Comment #557 by Johan on
Comment #558 by Johan on
Comment #9524 by Elías Guisado on
Comment #9790 by Elías Guisado on
There are also: