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 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.
Let be the canonical maps. Then we have the base change map of -modules
.
where is induced by . Since is coherent, we can identify with . Since is also coherent (as f is proper), doing the same identification, the above reads:
.
Using where and , one also obtains (after passing to limit):
where are as before. The composition of the two maps is the one in the lede. (To see that the map we constructed is the same one as in EGA, see EGA III-1.)
Notes
^EGA III-1, 4.1.5 harvnb error: no target: CITEREFEGA_III-1 (help)
^EGA III-1, 4.2.1 harvnb error: no target: CITEREFEGA_III-1 (help)
^Hartshorne, Ch. III. Corollary 11.2 harvnb error: no target: CITEREFHartshorne (help)
^Hartshorne, Ch. III. Corollary 11.3 harvnb error: no target: CITEREFHartshorne (help)