Bill Lawvere writes: With the experience of the last decades, it should be possible to explain how Zermelo???s theorem "in a base topos" was sufficient to the need of his friend Reinhold Baer. (Lifting the basic case to modules and sheaves is routinely done with suitable right adjoint functors.) I think everybody loved Reinhold Baer. I first spent time with him one week in Warsaw. A few years later I helped him secure his (retirement) apartment in Zurich (by renting it for 6 months). And somehow I just never got around to telling him the easy way to construct injective modules. The suitable right-adjoint functors -- that Bill mentions -- tell one how to construct an injective cogenerator for R-modules but neither the construction nor the proof of injectiviy need mention anything about functors: it???s pretty easy to show that any divisible abelian group is injective (with one use of Zorn???s lemma): after deciding whether it???s left or right R-modules you???re talking about, take the set of abelian-group maps from R to Q/Z and view it as an R-module. Done. And no more need of the axiom of choice. The R-module homomorphisms from M to this construction are in easy one-to-one correspondence with the abelian-group homomorphisms from M to Q/Z. (With a little work you can do the same for the category of additive functors from a small abelian category to the category of abelian groups. No ordinal numbers in sight.) As for Bill???s question: For deriving functors, Godement used resolving sheaves more concrete than injective ones, but Grothendieck preferred the latter. When do they exit? Well, in the Forward of the 2003 TAC version of "Abelian Categories" I wrote (on page -15): Pages 131-132: The very large category _B_ (Exercise 6A) -- with a few variations -- has been a great source of counterexamples over the years. As pointed out above (concerning pages 85-86) the forgetful functor is bi-continuous but does not have either adjoint. To move into a more general setting [to obtain a topos _C_ instead of an abelian category], drop the condition that G be a group and rewrite the convention to become f(y) = 1_G for y not in S (and, of course, drop the condition that h be a homomorphism -- it can be any function). The result is a category that satisfies all the conditions of a Grothendieck topos except for the existence of a generating set. It is not a topos: the subobject classifier would need to be the size of the universe. If we require, instead, that all the values of f be permutations, it is a topos and a boolean one at that. Indeed, the forgetful functor preserves all the relevant structure (in particular, Omega has just two elements). In its category of abelian-group objects Ext(A,B) is a proper class iff there???s a non-zero group homomorphism from A to B (it needn???t respect the actions), hence the only injective object is the zero object (which settled a once-open problem [years ago] about whether there are enough injectives in the category of abelian groups in every elementary topos with natural-numbers object). http://www.tac.mta.ca/tac/reprints/articles/3/tr3.pdf On the subject of the need for choice, while there take a look at the very last item in my 2003 Forward (page -14). The embedding theorem for abelian categories is an easy consequence of an embedding theorem for regular categories and for that there???s a choice-free proof. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]