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.