In algebraic geometry, the theorem on formal functions states the following:
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
where the completion on the left is with respect to
Corollary: Let r be such that
Corollay: For each
Corollary: If
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
where
Using
where