Constructively, is the unit of the “free abelian group” monad on sets injective?

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

I'd like to present a more modular proof. The key lemma (which I learnt from Christian Sattler) is that any set $X$ is a filtered colimit of finite sets. Indeed, let $I$ be the category of pairs $(n, f)$ with $n \in \mathbb N$ and $f : [n] \to X$, where a morphism $(n, f) \to (m, g)$ is a function $p : [n] \to [m]$ such that $f = g \circ p$. Since the category of finite sets has finite colimits, so does $I$, and so in particular $I$ is filtered. Now $X$ is the colimit $\mathop{\mathrm{colim}}_{(n,f) \in I} [n]$ in the obvious way.

The free abelian group functor $F$ commutes with colimits, being a left adjoint, so $FX \cong \mathop{\mathrm{colim}}_{(n,f) \in I} F[n]$. Moreover, the functor $U$ sending an abelian group to its underlying set commutes with filtered colimits, so $UFX \cong \mathop{\mathrm{colim}}_{(n,f) \in I} UF[n]$.

The unit maps $[n] \to UF[n]$ are injective since $[n]$ has decidable equality. Filtered colimits commute with pullbacks in sets, so they preserve monomorphisms. This means precisely that the unit map $X \to UFX$ is also injective, as needed.

If we look more closely at the characterisation of equality in a filtered colimit of sets, we obtain an explicit description of $UFX$ as in previous answers.

Answer 2

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.

Answer 3

Yes; this is given in Mines, Richman, Ruitenburg, A course in constructive algebra, on p.54, stated just before Lemma 4.1, and proved in that lemma by a Church-Rosser argument. (Thanks to Thierry Coquand for pointing me to this proof.)

Answer 4

Yes! Here is a proof which is slightly different from both your proof and the proof in Mines–Richman–Ruitenberg.

First define the similarity relation on $\mathrm{List}(R \times X)$ as in Mines–Richman–Ruitenberg as the smallest equivalence relation generated by their clauses (i), (ii) and (iii). I'd argue that this is the obvious thing to do if you set out to construct the free module.

We'll then show: Lists $[\langle a_1, x_1\rangle, \ldots, \langle a_n, x_n \rangle]$ and $[\langle b_1, y_1\rangle, \ldots, \langle b_m, y_m \rangle]$ are similar if and only if for all $x \in X$, $I \subseteq \{1,\ldots,n\}$, $J \subseteq \{1,\ldots,m\}$ (I just mean the detachable subsets here) such that $x_i = x$ for all $i \in I$ and $y_j = x$ for all $j \in J$, there are supersets $I' \supseteq I$ and $J' \supseteq J$ (again, $I'$ and $J'$ should be detachable) such that $x_i = x$ for all $i \in I'$, $y_j = x$ for all $j \in J'$ and $\sum_{i \in I'} a_i = \sum_{j \in J'} b_j$.

This is done in three steps:

1. The proposed characterization of similarity defines an equivalence relation (transitivity is slightly nontrivial, as in your proof).
2. That equivalence relation encompasses similarity.
3. It is the smallest equivalence relation satisfying (i), (ii) and (iii). For this step to work, it's important that the additive group of the ring is (as all groups are) cancellative. That is, this step wouldn't generalize to rigs $(R,0,1,+,\cdot)$ where $(R,0,+)$ is just required to be a commutative monoid.

With the characterization of similarity in hand, the injectivity of the unit is then easy to establish: Assume that the lists $[\langle 1, x_1\rangle]$ and $[\langle 1, y_1\rangle]$ are similar. By the characterization (applied to $x_1$, $I = \{1\}$, $J = \emptyset$), there is a detachable set $J' \subseteq \{1\}$ such that $y_j = x_1$ for all $j \in J'$ and $1 = \sum_{j \in J'} 1$. We have $1 \in J'$ or $1 \not\in J'$. If $1 \not\in J'$, then $1 = 0$ in $R$; a contradiction. Thus $1 \in J'$. So $y_1 = x_1$.

Edit. Here are details on step 3. Let $({\approx})$ be the equivalance relation given by the proposed characterization. Let $({\sim})$ be an equivalence relation on $\mathrm{List}(R \times X)$ which satisfies clauses (i), (ii) and (iii). We verify $v \approx w \Rightarrow v \sim w$ by induction on the combined length of $v$ and $w$. The base case ($v = w = [] = \text{empty list}$) is immediate.

Now let lists $v$ and $w$ be given such that $v \approx w$ and such that at least one of the lists, let's say $v$, has positive length. Write $v = [\langle a_1,x_1\rangle, \ldots, \langle a_n,x_n \rangle]$ and $w = [\langle b_1,y_1\rangle, \ldots, \langle b_m,x_m \rangle]$. The definition of $v \approx w$ (applied to $x = x_1$, $I = \{1\}$, $J = \emptyset$) yields index sets $I'$ and $J'$ such that $x_i = x_1$ for all $i \in I'$, $y_j = x_1$ for all $j \in J'$, $c := \sum_{i \in I'} a_i = \sum_{j \in J'} b_j$. Let $\hat v$ and $\hat w$ be obtained from $v$ and $w$ by removing all those entries whose index is an element of $I'$ respectively $J'$. We claim:

(a) $\hat v \approx \hat w$

(b) $v \sim w$

Claim (b) follows from claim (a): If $\hat v \approx \hat w$, then by induction also $\hat v \sim \hat w$. Then also $(\langle c,x_1\rangle :: \hat v) \sim (\langle c,x_1\rangle :: \hat w)$ (where $({::})$ is adding an element in front). Since $({\sim})$ satisfies (i), (ii) and (iii), $v \sim w$.

On to claim (a). Let $x \in X$. Let $\hat I$ and $\hat J$ be (detachable) sets of indices of entries of $\hat v$ respectively $\hat w$ such that the corresponding entries mention $x$. These index sets can also be seen as subsets of $\{1,\ldots,n\}$ respectively $\{1,\ldots,m\}$, by slightly juggling the indices. Therefore the definition of $v \approx w$ yields index sets $I''$ and $J''$. It might be the case that $I''$ and $J''$ contain only indices which can be reinterpreted to be indices in $\hat v$ respectively $\hat w$. In this case we are done.

But it could also happen that $I''$ has nontrivial overlap with $I'$ or that $J''$ has nontrivial overlap with $J'$. In this case $I''$ and $J''$ are of no further use, but we learned that $x = x_1$. We now apply the definition of $v \approx w$ again, this time to $x_1$, $\hat I \cup I'$ and $\hat J \cup J'$ (where we first juggle the indices in $\hat I$ and $\hat J$ accordingly before taking the union). This gives us index sets $I'''$ and $J'''$. We have $\sum_{i \in I'''} a_i = \sum_{j \in J'''} b_j$. By cancellativity, also $\sum_{i \in I''''} a_i = \sum_{j \in J''''} b_j$ where $I'''' = I''' \setminus I'$ and $J'''' = J''' \setminus J'$. Hence we're done.

Answer 5

Here's yet another construction of the free abelian group on an arbitrary set, and a proof of the claim. I haven't seen the proof in Mines, Richman, Ruitenburg so I don't know how similar this is to that.

We define the free abelian group on a set $A$ to be a quotient $X/\sim$. The set $X$ is the set of all triplets $(n, f, x)$ where $n$ is a natural number, $f : [n] \to A$, where $[n] = \{0, 1, \dots, n-1\}$, and $x \in \mathbb {Z}^n$. The equivalence $(n, f, x) \sim (m, g, y)$ holds if there is some $k \in \mathbb {N}$, $r : [k] \to A$ and maps $i : [n] \to [k]$, $j : [m] \to [k]$ such that $f = r \circ i$, $g = r \circ j$, $i^* (x) = j^* (y)$, where $i^* : \mathbb {Z}^n \to \mathbb {Z}^k$ is the linear map that takes the basis element $e^{(n)}_t \in \mathbb {Z}^n$ to $e^{(k)}_{i (t)} \in \mathbb {Z}^k$, and similarly for $j^*$. This relation is transitive since if also $(m, g, y) \sim (p, h, z)$ via $[m] \xrightarrow {i'} [\ell] \xleftarrow {j'} [p]$, then the pushout of $(j, i')$ is some finite set $[u]$ with maps $[k] \xrightarrow {i''} [u] \xleftarrow {j''} [\ell]$, and then $i'' \circ i : [n] \to [u]$, $j'' \circ j' : [p] \to [u]$ exhibit an equivalence $(n, f, x) \sim (p, h, z)$. Note the crucial use of the existence of pushouts in the category of finite sets. Sums are defined by $(n, f, x) + (m, g, y) = (n+m, f \oplus g, (x,y))$, where $f \oplus g : [n+m] \simeq [n] \sqcup [m] \to A$ is the concatenation of $f$ and $g$, and similarly $(x, y) \in \mathbb {Z}^{n+m}$ is concatenation. I won't bother verifying the abelian group laws.

More abstractly, the free abelian group generated by $A$ as a set is the colimit over the category of finite multisets in $A$ of the free abelian groups generated by them, where a finite multiset in $A$ is a map $[n] \to A$. This suggests a generalization to arbitrary Lawvere theories.

To prove the claim that $A \to \mathbb {Z} [A]$ is injective, note that the generator corresponding to $a \in A$ is given by $t (a) = (1, (0 \mapsto a), (1)) \in X$. If $t (a) \sim t (b)$ via the maps $[1] \xrightarrow {i} [k] \xleftarrow {j} [1]$ and $h : [k] \to A$, then $i^* (1) = j^* (1) \in \mathbb {Z}^k$ implies that $i (0) = j (0)$, and hence $a = h (i (0)) = h (j (0)) = b$.