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$

Proof. Namely, if $(r, h, k)$ is a formal homotopy between $f_1$ and $f_2$, then $(r, h, g \circ k)$ is a formal homotopy between $g \circ f_1$ and $g \circ f_2$. $\square$

Proof. By Theorem 90.26.4 and its proof, $\mathcal{F}$ has a presentation by a smooth prorepresentable groupoid

in functors on $\mathcal{C}_\lambda$ such that $\mathcal{F}$. Then the maps $s : R \to R_1$ and $t : R \to R_1$ are formally smooth ring maps and $e : R_1 \to R$ is a section. In particular, we can choose an isomorphism $R_1 = R[[t_1, \ldots , t_ r]]$ for some $r \geq 0$ such that $s$ is the embedding $R \subset R[[t_1, \ldots , t_ r]]$ and $t$ corresponds to a map $h : R \to R[[t_1, \ldots , t_ r]]$ with $h(a) \bmod (t_1, \ldots , t_ r) = a$ for all $a \in R$. The existence of the isomorphism $\alpha : f_*\xi \to g_*\xi$ means exactly that there is a map $k : R_1 \to S$ such that $f = k \circ s$ and $g = k \circ t$. This exactly means that $(r, h, k)$ is a formal homotopy between $f$ and $g$. $\square$

Proof. Suppose $(r, h, k)$ is a formal homotopy between $f_1$ and $f_2$. We claim that $\mathfrak pR[[t_1, \ldots , t_ r]] = h(\mathfrak p)R[[t_1, \ldots , t_ r]]$. The claim implies the lemma by further composing with $k$. To prove the claim, observe that the map $\mathfrak p \mapsto \mathfrak pR[[t_1, \ldots , t_ r]]$ is a bijection between the minimal prime ideals of $R$ and the minimal prime ideals of $R[[t_1, \ldots , t_ r]]$. Finally, $h(\mathfrak p)R[[t_1, \ldots , t_ r]]$ is a minimal prime as $h$ is flat, and hence of the form $\mathfrak q R[[t_1, \ldots , t_ r]]$ for some minimal prime $\mathfrak q \subset R$ by what we just said. But since $h \bmod (t_1, \ldots , t_ r) = \text{id}_ R$ by definition of a formal homotopy, we conclude that $\mathfrak q = \mathfrak p$ as desired. $\square$