Bounded below complexes admit injective replacements

Start with $I^j=0$ below $a$. Maintain the complex and monic map through degree $n$, cohomology isomorphisms below $n$, and a monomorphism $\mathrm{coker}{d}_X^{n-1}\to \mathrm{coker}{d}_I^{n-1}$. At $n=a-1$ all these data are zero.

Form the pushout $E=X^{n+1}{⨿}_{\mathrm{coker}{d}_X^{n-1}}\mathrm{coker}{d}_I^{n-1}$, using the map to $X^{n+1}$ induced by $d_X^n$. Choose $E\hookrightarrow I^{n+1}$ injective. The component $X^{n+1}\to I^{n+1}$ is monic by pushout stability, and $I^n\to \mathrm{coker}{d}_I^{n-1}\to I^{n+1}$ is the differential. The square commutes and consecutive differentials compose to zero.

The pushout kernel and cokernel identities give a monomorphism on the next cokernels and an isomorphism on $H^n$: explicitly this is the arrow-reversal of the pullback identities for cycles and boundaries, with kernels exchanged for cokernels, epis for monos, and degree $n$ exchanged for $-n$. The pushout identifies the quotient of the new ambient cokernel by the old one with the corresponding quotient for $X$; its kernel identity gives equality of the remaining cohomology subquotients. Thus the maintained conditions hold at $n+1$.

DC produces the ascending sequence of stages, or the supplied embeddings do. If object choices form a definable class, recursively bound ranks of extensions of each node by the least rank admitting one, bound over the set of nodes using Replacement, and take the set of all bounded extensions at the next stage. The union of these stage sets is a set to which DC applies. Every fixed degree then stabilizes and its cohomology comparison is an isomorphism. Finally $X\to {\tau }^{\ge a}X$ handles a merely cohomological lower bound before this construction. No class-indexed choice of $I_X$ is inferred.