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)