Proof.
Let A \mapsto (A \to J(A)) be a functorial injective embedding, see Homology, Definition 12.27.5. We first note that we may assume J(0) = 0. Namely, if not then for any object A we have 0 \to A \to 0 which gives a direct sum decomposition J(A) = J(0) \oplus \mathop{\mathrm{Ker}}(J(A) \to J(0)). Note that the functorial morphism A \to J(A) has to map into the second summand. Hence we can replace our functor by J'(A) = \mathop{\mathrm{Ker}}(J(A) \to J(0)) if needed.
Let K^\bullet be a bounded below complex of \mathcal{A}. Say K^ p = 0 if p < B. We are going to construct a double complex I^{\bullet , \bullet } of injectives, together with a map \alpha : K^\bullet \to I^{\bullet , 0} such that \alpha induces a quasi-isomorphism of K^\bullet with the associated total complex of I^{\bullet , \bullet }. First we set I^{p, q} = 0 whenever q < 0. Next, we set I^{p, 0} = J(K^ p) and \alpha ^ p : K^ p \to I^{p, 0} the functorial embedding. Since J is a functor we see that I^{\bullet , 0} is a complex and that \alpha is a morphism of complexes. Each \alpha ^ p is injective. And I^{p, 0} = 0 for p < B because J(0) = 0. Next, we set I^{p, 1} = J(\mathop{\mathrm{Coker}}(K^ p \to I^{p, 0})). Again by functoriality we see that I^{\bullet , 1} is a complex. And again we get that I^{p, 1} = 0 for p < B. It is also clear that K^ p maps isomorphically onto \mathop{\mathrm{Ker}}(I^{p, 0} \to I^{p, 1}). As our third step we take I^{p, 2} = J(\mathop{\mathrm{Coker}}(I^{p, 0} \to I^{p, 1})). And so on and so forth.
At this point we can apply Homology, Lemma 12.25.4 to get that the map
\alpha : K^\bullet \longrightarrow \text{Tot}(I^{\bullet , \bullet })
is a quasi-isomorphism. To prove we get a functor inj it rests to show that the construction above is functorial. This verification is omitted.
Suppose we have a functor inj such that s \circ inj = \text{id}. For every object K^\bullet of \text{Comp}^{+}(\mathcal{A}) we can write
inj(K^\bullet ) = (i_{K^\bullet } : K^\bullet \to j(K^\bullet ))
This provides us with a resolution functor as in Definition 13.23.2.
\square
Comments (0)