Enough injective abelian sheaves

By [F1] the category $\mathrm{A}\mathrm{b}(X)$ is a locally small Grothendieck category; applying [F2] and [F3], whose only hypothesis is AC, gives a functorial monomorphism ${\eta }_M:M\rightarrowtail E(M)$ into an injective object for every object $M$ of $\mathrm{A}\mathrm{b}(X)$, and shows that $\mathrm{A}\mathrm{b}(X)$ has enough injectives and that every abelian sheaf admits an injective resolution.

Fix an abelian sheaf $\mathcal{F}$. Set $I^0(\mathcal{F}):=E(\mathcal{F})$ and ${\eta }^0:={\eta }_{\mathcal{F}}$. Suppose a coaugmented complex $0\to \mathcal{F}\stackrel{\eta }{\to }{I}^0\to \cdots \to I^n$ has been constructed which is exact at every displayed term except possibly at $I^n$, with all $I^j$ injective. Let $C^n:=\mathrm{coker}(I^{n-1}\to I^n)$ for $n\ge 1$ and $C^0:=\mathrm{coker}(\eta )$. Put $I^{n+1}(\mathcal{F}):=E(C^n)$ and $j:={\eta }_{C^n}:C^n\rightarrowtail I^{n+1}(\mathcal{F})$, which is a monomorphism into an injective object by step 1.1. By [F4] the composite $I^n\twoheadrightarrow C^n\stackrel{j}{\to }{I}^{n+1}(\mathcal{F})$ extends the complex by one term and makes it exact at $I^n$; all displayed terms of the extended complex are injective. [F4, step 1.1, construct]

Recursing the construction of step 2.1 over $n=0,1,2,\dots$ (each step uses only the already constructed complex, so no simultaneous choices are made) produces an injective resolution $0\to \mathcal{F}\to I^0(\mathcal{F})\to I^1(\mathcal{F})\to \cdots$ of $\mathcal{F}$: it is exact at $\mathcal{F}$ because ${\eta }^0$ is a monomorphism, and exact at each $I^n$ by construction. [step 2.1, construct]

The recursion of step 2.1 is a rule depending only on the object $\mathcal{F}$: at every stage it applies the fixed functorial embedding $E$ of [F2] to the canonical cokernel of the previously constructed map, so it selects no resolutions, no embeddings and no representatives. Hence $\mathcal{F}\mapsto I^{\bullet }(\mathcal{F})$ is one specific assignment of an injective resolution to each abelian sheaf, i.e. a supplied injective resolution datum on all of $\mathrm{A}\mathrm{b}(X)$ in the sense of [F5]. [F2, F5, step 2.1]

Together, step 1.1 gives enough injectives and that every abelian sheaf admits an injective resolution, step 3.1 gives the resolutions of this construction, and step 3.2 exhibits them as a single supplied functorial datum; the Axiom of Choice is used only through the functorial embedding [F2] and the corollary [F3], and nowhere else.