# Theorem on formal functions

In algebraic geometry, the theorem on formal functions states the following:
    Let $f:X\to S$ be a proper morphism of noetherian schemes with a coherent sheaf ${\mathcal {F}}$ on X. Let $S_{0}$ be a closed subscheme of S defined by ${\mathcal {I}}$ and ${\widehat {X}},{\widehat {S}}$ formal completions with respect to $X_{0}=f^{-1}(S_{0})$ and $S_{0}$. Then for each $p\geq 0$ the canonical (continuous) map:
       $(R^{p}f_{*}{\mathcal {F}})^{\wedge }\to \varprojlim _{k}R^{p}f_{*}{\mathcal {F}}_{k}$
    is an isomorphism of (topological) ${\mathcal {O}}_{\widehat {S}}$-modules, where
   * The left term is $\varprojlim R^{p}f_{*}{\mathcal {F}}\otimes _{{\mathcal {O}}_{S}}{\mathcal {O}}_{S}/{{\mathcal {I}}^{k+1}}$.
   * ${\mathcal {F}}_{k}={\mathcal {F}}\otimes _{{\mathcal {O}}_{S}}({\mathcal {O}}_{S}/{\mathcal {I}}^{k+1})$
   * The canonical map is one obtained by passage to limit.
The theorem is used to deduce some other important theorems: Stein factorization and a version of Zariski's main theorem that says that a proper birational morphism into a normal variety is an isomorphism. Some other corollaries (with the notations as above) are:
Corollary: For any $s\in S$, topologically,
    $((R^{p}f_{*}{\mathcal {F}})_{s})^{\wedge }\simeq \varprojlim H^{p}(f^{-1}(s),{\mathcal {F}}\otimes _{{\mathcal {O}}_{S}}({\mathcal {O}}_{s}/{\mathfrak {m}}_{s}^{k}))$
where the completion on the left is with respect to ${\mathfrak {m}}_{s}$.
Corollary: Let r be such that $\operatorname {dim} f^{-1}(s)\leq r$ for all $s\in S$. Then
    $R^{i}f_{*}{\mathcal {F}}=0,\quad i>r.$
Corollay: For each $s\in S$, there exists an open neighborhood U of s such that
    $R^{i}f_{*}{\mathcal {F}}|_{U}=0,\quad i>\operatorname {dim} f^{-1}(s).$
Corollary: If $f_{*}{\mathcal {O}}_{X}={\mathcal {O}}_{S}$, then $f^{-1}(s)$ is connected for all $s\in S$.
The theorem also leads to the Grothendieck existence theorem, which gives an equivalence between the category of coherent sheaves on a scheme and the category of coherent sheaves on its formal completion (in particular, it yields algebralizability.)
Finally, it is possible to weaken the hypothesis in the theorem; cf. Illusie. According to Illusie (pg. 204), the proof given in EGA III is due to Serre. The original proof (due to Grothendieck) was never published.

## The construction of the canonical map

Let the setting be as in the lede. In the proof one uses the following alternative definition of the canonical map.
Let $i':{\widehat {X}}\to X,i:{\widehat {S}}\to S$ be the canonical maps. Then we have the base change map of ${\mathcal {O}}_{\widehat {S}}$-modules
    $i^{*}R^{q}f_{*}{\mathcal {F}}\to R^{p}{\widehat {f}}_{*}(i'^{*}{\mathcal {F}})$.
where ${\widehat {f}}:{\widehat {X}}\to {\widehat {S}}$ is induced by $f:X\to S$. Since ${\mathcal {F}}$ is coherent, we can identify $i'^{*}{\mathcal {F}}$ with ${\widehat {\mathcal {F}}}$. Since $R^{q}f_{*}{\mathcal {F}}$ is also coherent (as f is proper), doing the same identification, the above reads:
    $(R^{q}f_{*}{\mathcal {F}})^{\wedge }\to R^{p}{\widehat {f}}_{*}{\widehat {\mathcal {F}}}$.
Using $f:X_{n}\to S_{n}$ where $X_{n}=(X_{0},{\mathcal {O}}_{X}/{\mathcal {J}}^{n+1})$ and $S_{n}=(S_{0},{\mathcal {O}}_{S}/{\mathcal {I}}^{n+1})$, one also obtains (after passing to limit):
    $R^{q}{\widehat {f}}_{*}{\widehat {\mathcal {F}}}\to \varprojlim R^{p}f_{*}{\mathcal {F}}_{n}$
where ${\mathcal {F}}_{n}$ are as before. One can verify that the composition of the two maps is the same map in the lede. (cf. EGA III-1, section 4)