In algebraic geometry, the theorem on formal functions states the following:[1]
- Let
be a proper morphism of noetherian schemes with a coherent sheaf
on X. Let
be a closed subscheme of S defined by
and
formal completions with respect to
and
. Then for each
the canonical (continuous) map:

- is an isomorphism of (topological)
-modules, where
- The left term is
.

- 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:[2] For any
, topologically,

where the completion on the left is with respect to
.
Corollary:[3] Let r be such that
for all
. Then

Corollay:[4] For each
, there exists an open neighborhood U of s such that

Corollary:[5] If
, then
is connected for all
.
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.