Construction of injective hulls without axiom of choice

Question

Motivation: It is known that without the axiom of choice (AC), it is not provable that all categories of modules have enough injectives, let alone injective hulls. Still, there are examples of rings where one can explicitly write down 'candidate' embeddings which can be proved to be injective hulls using AC; e.g. over ${\mathbb Z}$, one can at least write down ${\mathbb Z}\to{\mathbb Q}$ as a candidate for an injective hull, even though one needs AC to show that ${\mathbb Q}$ is injective.

I'm wondering whether this explicit construction of 'candidate' embeddings that turn out to be injective hulls using AC is always possible, or if there are injective hulls whose underlying embeddings one cannot even write down without AC. Here's an attempt to make this question precise:

Intuitive Question: Given a module $M$ over a ring $R$, I would like to know whether it is possible in $\textsf{ZF}$ to construct a pair $(I,\iota)$ consisting of another $R$-module $I$ and a map $\iota: M\to I$ which $\textsf{ZFC}$ proves to be an injective hull of $M$.

Attempt to formalize: Is there a formula $\psi(R,M,I,\iota)$ in the language of set theory, such that $$\textsf{ZF}\ \vdash\ \text{Ring}(R)\wedge\text{Mod}(R,M)\Rightarrow(\exists! I,\iota: \psi(R,M,I,\iota))\wedge(\forall I,\iota: \psi(R,M,I,\iota)\Rightarrow (\text{Mod}(R,I)\wedge\text{ModHom}(R,M,I,\iota))),\\[4mm]\textsf{ZFC}\ \vdash\ \text{Ring}(R)\wedge\text{Mod}(R,M)\wedge\psi(R,M,I,\iota)\Rightarrow\text{InjHull}(R,M,I,\iota)$$

In other words: Is it the existence of the underlying modules of the injectives that is problematic without AC, or rather the proof of their injectivity?

Answer 1

No, there is no such formula, even restricting to $R=\mathbb Z$ and modules $M$ isomorphic to $\mathbb Z/8\mathbb Z.$ $\DeclareMathOperator{Aut}{Aut}$

I think your formulation is fine as it is. The choiceless part actually plays no role because the formula can just specify $I=M$ whenever AC does not hold. So the question is about definability in ZFC. To allow a rigorous argument without getting into technicalities, for now I’ll take the set theory to be ZFCA - ZFC with atoms/urelements.

My reference for set theory is Jech’s Set Theory. The model of ZFCA I’ll use is a rather degenerate permutation model defined by a set of eight atoms $A=\{a_0,\dots,a_7\},$ the group $G$ of permutations fixing the group structure $a_i+a_j=a_{i+j\pmod 8},$ and the filter generated by the trivial group i.e. there’s no restriction to hereditarily symmetric sets. The elements of $G$ extend to automorphisms on the universe of sets.

Let $\iota:A\to I$ be the injective hull given by $\psi.$ We can pick isomorphisms of $A$ and $I$ with $\tfrac18 \mathbb Z/\mathbb Z$ and $\mathbb Q/\mathbb Z$ such that $\iota$ is the inclusion.

Each automorphism of $I$ restricts to an automorphism of $A$; this gives a map $$r:\Aut(\mathbb Q/\mathbb Z) \to \Aut(\tfrac18 \mathbb Z/\mathbb Z)$$ The group $G$ of automorphisms of $A$ act on $I,$ giving a map $$s:\Aut(\tfrac18 \mathbb Z/\mathbb Z) \to \Aut(\mathbb Q/\mathbb Z).$$

And $s$ is a section of $r$ because $r\circ s$ is just the action of $G$ on $A.$ The map $r$ factors through $\Aut(\tfrac1{16} \mathbb Z/\mathbb Z)=(\mathbb Z/16\mathbb Z)^\times,$ whose involutions $1,7,9,15\pmod{16}$ all map to $\pm 1$ in $(\mathbb Z/8\mathbb Z)^\times.$ So $r$ cannot have a section. More conceptually: $\Aut(\mathbb Q/\mathbb Z) \cong \widehat{\mathbb Z}^\times\cong \prod_p \mathbb Z_p^\times.$ Only the $2$-adics' units act nontrivially on $A,$ and their torsion group is $\{\pm 1\}.$

---

To get the same result in ZFC, force to add eight sets of $\omega$ Cohen reals, and use these sets as the atoms $a_0,\dots,a_7.$ The argument goes through analogously to classic symmetric model proofs; any forcing condition doesn’t tell you anything about which atom is which. To extend this to definability with parameters, use a class forcing and take atoms of higher rank than any parameter. I believe these arguments are quite standard and not worth dwelling on for this particular question.

---

It is tempting to think that definability is related to functoriality, making the inclusion maps $\iota$ the components of a natural transformation. But functoriality is a very strong condition. For example ZFC can define a class function taking non-empty sets $x$ to the identity map $x\to x$ and taking the empty set to the unique map $0\to 1.$ But this cannot be made functorial; see [1] Example 3.1.

---

Finally I would like to make some comments about injective resolutions. As you mentioned, these may not exist in ZF (see [2]). But ZFC has definable injective resolutions - the construction $J(M)$ in Stacks [2] for example is very explicit, and even functorial. (Unless I’m missing something, the construction even works for non-commutative rings.) The fact that injective modules may not exist in ZF is partly because the definition is very demanding in the absence of Choice. As an analogy, if you defined algebraic closures as “injective objects in the category of algebraic field extensions”, then ZF wouldn’t even prove that $\mathbb Q$ has an algebraic closure (because we then are requiring uniqueness not just existence). I haven't checked this at all carefully but: if we define “Baer-injective” modules using Baer’s criterion, then I think ZF has definable Baer-injective resolutions in the category of modules over a Noetherian ring (=every ideal is finitely generated). In particular, the category of abelian groups. Just take the directed colimit of the Stacks construction $J(M’)$ over finitely generated submodules $M'\subseteq M.$

[1] Jiří Adámek, Horst Herrlich, Jiří Rosický & Walter Tholen, Injective Hulls are not Natural, https://link.springer.com/article/10.1007/s000120200006

[2] Andreas Blass, Injectivity, Projectivity, and the Axiom of Choice, https://www.jstor.org/stable/1998165

[3] https://stacks.math.columbia.edu/tag/01D8