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

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.]

• I believe that the existence of such a constructive proof [constructively] follows from the existence of the classical proof, since we can apply the baby version of Barr's theorem (the double negation translation followed by Friedman's trick), as the claim can be formulated as a geometric sequent. Do you concur? – Ingo Blechschmidt Jun 11 '18 at 15:16
• @IngoBlechschmidt: I don’t see how to formulate the claim as a geometric sequent, I’m afraid — what did you have in mind? Given that, I agree with the rest of the argument. – Peter LeFanu Lumsdaine Jun 11 '18 at 19:00
• More generally (and more usefully), we should be able to prove that if $1_{a_1} + 1_{a_2} + \cdots + 1_{a_n} = 1_{b_1} + 1_{b_2} + \cdots + 1_{b_m}$ for some elements $a_1, a_2, \ldots, a_n, b_1, b_2, \ldots, b_m$ of $X$, then the list $\left(a_1, a_2, \ldots, a_n\right)$ is a permutation of the list $\left(b_1, b_2, \ldots, b_m\right)$ (in the concrete sense: i.e., we have $n = m$, and there is some permutation $\sigma$ of $\left\{1,2,\ldots,m\right\}$ such that each $i$ satisfies $a_i = b_{\sigma\left(i\right)}$). I have a hunch that this should ... – darij grinberg Jun 11 '18 at 19:50
• ... boil down to something like the Garsia-Milne involution principle: A crucial step is to show that if a tuple $\mathbf{a}$ is a permutation of a tuple $\mathbf{b}$, and some sub-tuple $\mathbf{a}'$ of $\mathbf{a}$ is a permutation of some sub-tuple $\mathbf{b}'$ of $\mathbf{b}$, then the complementary tuple of $\mathbf{a}'$ in $\mathbf{a}$ is a permutation of the complementary tuple of $\mathbf{b}'$ in $\mathbf{b}$. – darij grinberg Jun 11 '18 at 19:57
• The calculus of "combinatorial objects" in Nicholas A. Loehr, Anthony Mendes, Bijective matrix algebra, Linear Algebra and its Applications, Volume 416, Issues 2--3, 15 July 2006, pp. 917--944 also seems of relevance -- though the way they have built it up, it probably requires all the sets to have decidable equality. – darij grinberg Jun 11 '18 at 19:59

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.

• Very nice! By the way, outside category theory people might wonder if "holding on the nose" has anything to do with sea lions' juggling abilities. – Andrej Bauer Jun 11 '18 at 9:14
• @Andrej It means precisely that! – Harry Gindi Jun 11 '18 at 9:49
• Thanks very much for writing out the details, Peter. Is there a general class of algebraic theories one can name where the unit of the monad is injective, constructively? – Todd Trimble Jun 11 '18 at 12:14
• @ToddTrimble If an algebraic theory is generated by some function symbols and some relations, I would think we can express elements of the free object as lists of the union of the set of function symbols and elements of the base set (say in reverse Polish notation), satisfying some rules, up to an equivalence relation of chains of valid algebraic manipulations using the relations. Expressed this way, I would think that it holds constructively if and only if it holds in the usual mathematics, because the only way to make two things equivalent is by an explicit construction. – Will Sawin Jun 11 '18 at 19:55
• @WillSawin: trees, use trees instead of lists. Peter is using lists because he can juggle associativity on his nose. – Andrej Bauer Jun 11 '18 at 20:29

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.)

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.

• Very nice alternate characterisation! Could you expand on the argument you had in mind for your step 3? The only argument I am seeing for it right now is to show that your notion of similarity implies mine, but I guess this isn’t what you had in mind since (a) it would make your answer unnecessarily dependent on mine, and (b) (if I’m not mistaken) that argument then doesn’t require cancellativity but works fine also for pseudo-rings (i.e. what I called rigs in my answer). – Peter LeFanu Lumsdaine Jun 11 '18 at 16:16
• When you say $0 \in J'$, you mean $1 \in J'$? – darij grinberg Jun 11 '18 at 19:46
• @Peter: I added a few details, and would like to apologize for the messy index-heavy proof. (In German we have a term for this: "Indexschlacht", literally "index battle".) Also thanks for reminding me of the proper notion, I changed "pseudo-ring" to "rig" to not contribute to unnecessary proliferation of terms. Darij: Yes, indeed, thank you; fixed. – Ingo Blechschmidt Jun 12 '18 at 11:45

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 $ \xrightarrow {i} [k] \xleftarrow {j} $ 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$.

• Very nice! Unlike mine and like Peter's, your proof doesn't require cancellability, so generalizes to modules over rigs. In fact, I believe that your proof can be homotoped to Peter's proof. – Ingo Blechschmidt Jun 12 '18 at 12:20
• @IngoBlechschmidt: I agree this is another nice alternative description of the equivalence relation, but I don’t think your or my characterisations require cancellativity? At least mine doesn’t, unless I have made an error somewhere (I state it for rigs from the start!), and the indirect argument I had for yours doesn’t either (showing that your relation implies mine, by inductively building up a colouring by repeatedly using your criterion on any remaining “uncoloured” elements)? – Peter LeFanu Lumsdaine Jun 14 '18 at 12:08