The free abelian group monad The forgetful functor $U : \mathsf{Ab} \to \mathsf{Set}$ is monadic, this follows from Beck's monadicity theorem or some other general result. Anyway, I would like to prove this directly, thereby solving an exercise in Mac Lane's Categories for the working mathematician. This amounts to prove an equivalent definition of an abelian group, using $\mathbb{Z}$-linear combinations of arbitrary length, which should be quite elementary. But working through the details, I get stuck at some point.
First, let me describe the monad $T: \mathsf{Set} \to \mathsf{Set}$ corresponding to $U$. It maps a set $X$ to the set $T(X)$ of functions $\lambda : X \to \mathbb{Z}$ with finite support. If $f : X \to Y$ is a map, then $T(X) \to T(Y)$ sends $\lambda$ to the function $y \mapsto \sum_{x \in f^{-1}(y)} \lambda(x)$. The unit $\eta : \mathrm{id} \to T$ sends $x \in X$ to the function supported at $x$ with value $1$. The multiplication $\mu : T^2 \to T$ maps $\alpha \in T^2(X)$ to $\mu(\alpha) \in T(X)$ defined by $\mu(\alpha)(x)=\sum_{\lambda \in T(X)} \alpha(\lambda) \cdot \lambda(x)$.
It follows that a $T$-module may be described as follows: This is a set $X$ together with a map $h : T(X) \to X$, which I will denote by $f \mapsto \sum_{x \in X} f(x) \cdot x$, such that the following properties hold:
1) If $f \in T(X)$ is supported at $x_0 \in X$ with value $1$, then $\sum_{x \in X} f(x) \cdot x = 1$.
2) For every $\alpha \in T(T(X))$ we have an equality
$$\sum_{x \in X} \Bigl(\sum_{\lambda \in T(X)} \alpha(\lambda) \cdot \lambda(x)\Bigr) \cdot x = \sum_{x \in X} \Bigl(\sum_{\lambda \in T(X), \sum\limits_{y \in X} \lambda(y)=x} \alpha(\lambda)\Bigr) \cdot x$$
From the notation it is clear how the comparison functor $\mathsf{Ab} \to \mathsf{Mod}(T)$ looks like. Conversely, let $(X,h)$ be a $T$-module. Then I would like to define a binary operation $+$ on $X$ roughly by $x+y = 1 \cdot x + 1 \cdot y + 0 \cdot ? + \dotsc$. Unfortunately, the precise definition requires a case distinction! First, define $0_X := \sum_{x \in X} 0 \cdot x$. Then, for $x,y \in X$, define
$$x+y :=\begin{cases} \sum_{z \in X} \delta_{z,\{x,y\}} \cdot z & x \neq y\\ \sum_{z \in X} (2 \cdot \delta_{z,x}) \cdot z  & x = y \neq 0_M \\ 0_M & x=y=0_M \end{cases}$$
With such a definition, it seems to be very hard to prove associativity. Or is there an elegant proof? Or a better definition of $+$?
 A: The general strategy for these things is to regard $T (X)$ as being the set of all terms in the language of the algebraic theory in question, with variables drawn from $X$, modulo provable equality in that algebraic theory.  (I like to think this is the reason why monads are denoted by $T$; but probably the real reason is in the now-outdated name ‘triple’.) From this point of view, the action map $h : T (X) \to X$ interprets these formal terms as actual elements in $X$ in the obvious way. 
In particular, $T (X)$ will always have the structure of a $T$-algebra, and $h : T (X) \to X$ will always be a surjective $T$-algebra homomorphism, with a (set-theoretical) splitting $\eta_X : X \to T (X)$. Thus, the least painful way of defining the algebraic structure on $X$ is by lifting the elements of $X$ to $T (X)$ via $\eta$, using the algebraic operations of $T (X)$, and descending back to $X$ via $h$.
For example, if we define $T (X)$ to be the free abelian group on $X$ in the way you do, $T (X)$ is very easily seen to be an abelian group, so we can define the addition on $X$ by $x + y = h(\eta_X(x) + \eta_X(y))$. It now follows that $+$ is a unital commutative associative binary operation with two-sided inverses. For example,
\begin{align}
x + (y + z) & = h(\eta_X(x) + \eta_X(h(\eta_X(y) + \eta_X(z)))) \\
& = h(\eta_X(h(\eta_X(x))) +  \eta_X(h(\eta_X(y) + \eta_X(z)))) \\
& = h(T h (\eta_{T X}(\eta_X(x))) +  T h (\eta_{T X}(\eta_X(y) + \eta_X(z)))) \\
& = h(T h (\eta_{T X}(\eta_X(x)) + (\eta_{T X}(\eta_X(y) + \eta_X(z))))) \\
& = h(\mu_X (\eta_{T X}(\eta_X(x)) + (\eta_{T X}(\eta_X(y) + \eta_X(z))))) \\
& = h(\mu_X (\eta_{T X}(\eta_X(x))) +  \mu_X (\eta_{T X}(\eta_X(y) + \eta_X(z)))) \\
& = h(\eta_X (x) + (\eta_X (y) + \eta_X (z))) \\
& = h((\eta_X (x) + \eta_X (y)) + \eta_X (z)) \\
& \qquad\vdots \\
& = (x + y) + z
\end{align}
