Lemma 89.28.1. Being formally homotopic is an equivalence relation on sets of morphisms in $\widehat{\mathcal{C}}_\Lambda$.

Proof. Suppose we have any $r \geq 1$ and two maps $h_1, h_2 : R \to R[[t_1, \ldots , t_ r]]$ such that $h_1(a) \bmod (t_1, \ldots , t_ r) = h_2(a) \bmod (t_1, \ldots , t_ r) = a$ for all $a \in R$ and a map $k : R[[t_1, \ldots , t_ r]] \to S$. Then we claim $k \circ h_1$ is formally homotopic to $k \circ h_2$. The symmetric inherent in this claim will show that our notion of formally homotopic is symmetric. Namely, the map

$\Psi : R[[t_1, \ldots , t_ r]] \longrightarrow R[[t_1, \ldots , t_ r]],\quad \sum a_ I t^ I \longmapsto \sum h_1(a_ I)t^ I$

is an isomorphism. Set $h(a) = \Psi ^{-1}(h_2(a))$ for $a \in R$ and $k' = k \circ \Psi$, then we see that $(r, h, k')$ is a formal homotopy between $k \circ h_1$ and $k \circ h_2$, proving the claim

Say we have three maps $f_1, f_2, f_3 : R \to S$ as above and a formal homotopy $(r_1, h_1, k_1)$ between $f_1$ and $f_2$ and a formal homotopy $(r_2, h_2, k_2)$ between $f_3$ and $f_2$ (!). After relabeling the coordinates we may assume $h_2 : R \to R[[t_{r_1 + 1}, \ldots , t_{r_1 + r_2}]]$ and $k_2 : R[[t_{r_1 + 1}, \ldots , t_{r_1 + r_2}]] \to S$. By choosing a suitable isomorphism

$R[[t_1, \ldots , t_{r_1 + r_2}]] \longrightarrow R[[t_{r_1 + 1}, \ldots , t_{r_1 + r_2}]] \widehat{\otimes }_{h_2, R, h_1} R[[t_1, \ldots , t_{r_1}]]$

we may fit these maps into a commutative diagram

$\xymatrix{ R \ar[r]_{h_1} \ar[d]^{h_2} & R[[t_1, \ldots , t_{r_1}]] \ar[d]^{h_2'} \\ R[[t_{r_1 + 1}, \ldots , t_{r_1 + r_2}]] \ar[r]^{h_1'} & R[[t_1, \ldots , t_{r_1 + r_2}]] }$

with $h_2'(t_ i) = t_ i$ for $1 \leq i \leq r_1$ and $h_1'(t_ i) = t_ i$ for $r_1 + 1 \leq i \leq r_2$. Some details omitted. Since this diagram is a pushout in the category $\widehat{\mathcal{C}}_\Lambda$ (see proof of Lemma 89.4.3) and since $k_1 \circ h_1 = f_2 = k_2 \circ h_2$ we conclude there exists a map

$k : R[[t_1, \ldots , t_{r_1 + r_2}]] \to S$

with $k_1 = k \circ h_2'$ and $k_2 = k \circ h_1'$. Denote $h = h_1' \circ h_2 = h_2' \circ h_1$. Then we have

1. $k(h_1'(a)) = k_2(a) = f_3(a)$, and

2. $k(h_2'(a)) = k_1(a) = f_1(a)$.

By the claim in the first paragraph of the proof this shows that $f_1$ and $f_3$ are formally homotopic. $\square$

In your comment you can use Markdown and LaTeX style mathematics (enclose it like $\pi$). A preview option is available if you wish to see how it works out (just click on the eye in the toolbar).