Free Abelian Group Monad – Is the Unit Injective Constructively?

Question

Classically, we can explicitly construct the free Abelian group $\newcommand{\Z}{\mathbb{Z}}\Z[X]$ on a set $X$ as the set of finitely-supported functions $X \to \Z$, and so easily see that the unit map $X \to \Z[X]$ (inclusion of generators) is injective.

Constructively, this construction of $\Z[X]$ doesn’t work for arbitrary $X$. The unit map $X \to \Z[X]$ should send $x \in X$ to the function $1_x : X \to \Z$, sending $y \in X$ to $1$ if $y = x$ and $0$ otherwise; but this definition-by-cases requires that $X$ has decidable equality (i.e. for every $x,y \in X$, either $y = x$ or $y \neq x$).

Similarly, most other classical explicit constructions of $\Z[X]$ rely at some point on decidable equality of $X$. The abstract-nonsense syntactic construction of $\Z[X]$ as a free model of an algebraic theory works fine constructively; but from this construction, it’s not clear that the unit map $X \to \Z[X]$ is injective.

Is there some constructive proof that the unit map $X \to \Z[X]$ is injective for arbitrary $X$, or can it fail?

[Note this is a self-answered question. It came up since the fact was required here; asking several experts, the answer seems to be not well-known. After a couple of days, I worked out an answer via an explicit construction, and then also got a reply pointing to a slightly less explicit answer in the literature; so I’m writing it up here to make the answer and construction more prominently available.]

Answer 1

Yes! In fact, more generally, for any rig $R$ in which $0 \neq 1$, the map $X \mapsto R[X]$ is injective (where $R[X]$ denotes the free $R$-module on a set $X$).

Specifically: I claim we can construct $R[X]$ as a quotient of $\newcommand{\List}{\mathrm{List}}\List(R \times X)$, by an equivalence relation defined as follows:

Say lists $a$, $b$ are similar if there is some finite set $I$ (i.e. cardinal-finite), and an $I$-colouring of the entries of $a$ and of $b$ (i.e. functions $f_a : \{1,\ldots,l(a)\} \to I$ and $f_b : \{1,\ldots,l(b)\} \to I$), such that for each $i$ in $I$,

• (1) the $X$-components of all $i$-coloured entries of $a$ and $b$ are equal;
• (2) the sum of the coefficients (i.e. $R$-components) of all $i$-coloured entries of $a$ is the same as the sum of coefficients of $i$-coloured entries of $b$.

E.g. for any $x$, $y$ in $X$, the lists $(1x, 1y, -1x)$ and $(1y)$ are similar, witnessed by the 2-colouring of their positions as (red,blue,red) and (blue) respectively: all red entries have $X$-component $x$; all blue entries have $X$-component $y$; the sum of coefficients of red entries is $0$ in each list; the sum of coefficients of blue entries is $1$ in each list.

Compare to the simpler way one might classically define similarity, by saying “for each $x$ in $X$, the sum of coefficients of $x$ is the same in the two lists”. Constructively, we can’t take that sum unless $X$ has decidable equality: e.g. in the example above, taking the sum depends on knowing whether $x=y$ or $x \neq y$. But the colouring gives us extra data which is finite/decidable, so that we can take the required sums, and which is sufficient to witness that the lists should denote the same element of the free module.

Now we define “addition” on lists as concatenation, “0” as the empty list, and scalar multiplication as pointwise multiplication in the coefficients; and check that “similarity” is a congruence, and satisfies the module axioms:

• reflexivity: $a \sim a$ is witnessed by the “discrete” $l(a)$-colouring, where every entry has a different colour.
• symmetry: clear.
• transitivity: this is a bit tricky to describe. Suppose given an $I$-colouring $f$ witnessing $a\sim b$, and a $J$-colouring $g$ witnessing $b\sim c$. The idea now is to “merge overlapping colouring-classes in $b$, and then merge the classes in $a$ and $c$ correspondingly”. Precisely, look at the equivalence relation on $I+J$ generated by setting $i \simeq j$ if there’s an entry of $B$ coloured $i$ by $f$ and $j$ by $g$. This is decidable since it’s just a matter of finite computation on finite sets; so $K := (I+J)/{\simeq}$ is again finite. So now we get $K$-colourings of $a$ and $c$. These satisfy condition (1), since the merging was generated by merging classes that overlapped in $b$, and so must have already agreed on their $X$-components; and they satisfy condition (2) since for each new colour $k$, its class in $a$ is a union of classes of $f$ in $a$, and so the sum of coefficients over the class is the same as the sum of the corresponding classes of $f$ in $b$, which is exactly the class of $k$ in $b$; but symmetrically this is also the same as the sum of coefficients of the class of $k$ in $C$.
• respecting “addition”, i.e. concatenation: if $a \sim b$ and $c \sim d$, witnessed by an $I$-colouring and $J$-colouring respectively, then $ac \sim bd$ is witnessed by an obvious $(I+J)$-colouring.
• respecting scalar multiplication: any colouring witnessing $a \sim b$ will also still witness $ra \sim rb$.
• associativity of “addition”: holds on the nose.
• 0 as a unit for “addition”: holds on the nose.
• commutativity of “addition”: $ab \sim ba$ is witnessed by the evident discrete $(l(a)+l(b))$-colouring.
• distributivity of scalar multiplication over addition: holds on the nose.

So $\List(R \times X)/{\sim}$ is an $R$-module, with a map from $X$ given by sending $x$ in $X$ to the singleton list $(1x)$. And indeed it’s not hard to see explicitly that it’s free: any map $X \to M$ extends uniquely to a map on $\List(R \times X)$ respecting addition and scalar multiplication, and this extension must respect similarity.

Finally, if $1 \neq 0$ in $R$, then if $(1x) \sim (1y)$, any colouring witnessing this must give both entries the same colour (to satisfy the sum-of-coefficients condition), and so we must have $x = y$. So when $1 \neq 0$ in $R$, the map $X \to \List(R \times X)/{\sim}$ is injective.