In algebraic geometry, the theorem on formal functions states the following:
Let
f:X\toS
l{F}
S0
l{I}
\widehat{X},\widehat{S}
X0=f-1(S0)
S0
p\ge0
(Rpf*l{F})\wedge\to\varprojlimkRpf*l{F}k
is an isomorphism of (topological)
l{O}\widehat{S
\varprojlimRpf*l{F} ⊗ l{OS}
k+1 | |
l{O} | |
S/{l{I} |
l{F}k=l{F} ⊗ l{OS}
k+1 | |
(l{O} | |
S/{l{I}} |
)
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\inS
((Rpf*
\wedge | |
l{F}) | |
s) |
\simeq\varprojlimHp(f-1(s),l{F} ⊗ l{OS}(l{O}s/ak{m}
k)) | |
s |
ak{m}s
Corollary: Let r be such that
\operatorname{dim}f-1(s)\ler
s\inS
Rif*l{F}=0, i>r.
Corollay:[1] For each
s\inS
Rif*l{F}|U=0, i>\operatorname{dim}f-1(s).
Corollary: If
f*l{O}X=l{O}S
f-1(s)
s\inS
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.
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}\toX,i:\widehat{S}\toS
l{O}\widehat{S
i*Rqf*l{F}\toRp\widehat{f}*(i'*l{F})
\widehat{f}:\widehat{X}\to\widehat{S}
f:X\toS
l{F}
i'*l{F}
\widehat{l{F}}
Rqf*l{F}
(Rqf*l{F})\wedge\toRp\widehat{f}*\widehat{l{F}}
f:Xn\toSn
Xn=(X0,
n+1 | |
l{O} | |
X/l{J} |
)
Sn=(S0,
n+1 | |
l{O} | |
S/l{I} |
)
Rq\widehat{f}*\widehat{l{F}}\to\varprojlimRpf*l{F}n
l{F}n