The Stacks project

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

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

we may fit these maps into a commutative diagram

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 90.4.3) and since $k_1 \circ h_1 = f_2 = k_2 \circ h_2$ we conclude there exists a map

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$