Let $G$ be a group and let $F\xrightarrow\varepsilon\mathbb Z\to 0$ be the corresponding standard resolution, with $F_n=G^{n+1}$ and $\partial (s_0,\ldots,s_n)=\sum_{i=0}^n(-1)^i(s_0,\ldots,\hat s_i,\ldots,s_n)$.
I want to know if the following explicit homotopies that I found are already known.
For the first one, let $s\in G$. We consider the augmentation-preserving chain map $\tau_s:F\to F$, given by $(s_0,\ldots,s_n)\mapsto (s_0s,\ldots,s_ns)$. Then $\tau_s$ is homotopy equivalent to the identity, i.e. $\tau_s\approx 1$. What I want is an explicit homotopy from $\tau_s$ to $1$, i.e. a map $\phi_s:F\to F[1]$ such that $\tau_s-1=\partial\phi_s+\phi_s\partial$.
The homotopy $\psi_s$ which I found is given by $$\phi_s(s_0,\ldots,s_n)=\sum_{i=1}^n(-1)^i(s_0,\ldots,s_i,s_is,\ldots,s_ns).$$
The second one is about the augmentation-preserving chain map $\tau :F\otimes F\to F\otimes F$, given by $x\otimes y\mapsto (-1)^{pq}y\otimes x$ $\forall x\in F_p$, $y\in F_q$. Again, I want a homotpy from $\tau$ and $1$, i.e. a map $\phi :F\otimes F\to F\otimes F[1]$ such that $\tau -1=\partial\phi +\phi\partial$.
The homotopy $\phi$ that I found is given on $F_p\otimes F_q$ by $$\begin{aligned}\phi((s_0,\ldots,s_p)\otimes y) & =(-1)^{pq}\sum_{i=0}^p(-1)^{(q+1)i}(s_0,\ldots,s_i,y)\otimes (s_i,\ldots,s_p)\\ & \qquad\qquad -(-1)^p\sum_{i=0}^p(s_0,\ldots,s_i)\otimes (s_i,\ldots,s_p,y).\end{aligned}$$ (Here $y\in F_q$ has the form $y=(s_{p+1},\ldots,s_{p+q+1})$.)
I use these homotopies in the proof of the result I mentioned in my previous question:
