Using some filtered colimit nonsense we can reduce proper base change to and is -module for some fixed (there is no assumption on unlike smooth base change). We canfurther reduce to for some strictly Hensellian local ring . Then since taking global sections of sheaves on are exact (Stacks, 03QO), we see that we need to show is an isomorphism for all . Via some homological algebra we can reduced to showing it is an isomorphism for and surjective for . For it boils down to lifting idempotents, and applying the theorem on formal functions (which roughly says that taking cohomology commutes with completion, note that the properness hypothesis is crucial, e.g. if we take then is much smaller than the inverse limit of , which turns out to be , the ring of converging power series in the Gauss norm). For the proof of theorem on formal theorem, see here and here. Quote from the blog post: In fact, this is a very important point: the formal function theorem allows one to make a comparison with the cohomology of a given sheaf over the entire space and its cohomology over an “infinitesimal neighborhood” of a given closed subset. Now localization always commutes with cohomology on non-pathological schemes. However, taking such “infinitesimal neighborhoods” is generally too fine a job for localization. This is why the formal function theorem is such a big deal.
Well, first of all, completion is only really well-behaved for finitely generated modules. So we should have some condition that the cohomology groups are finitely generated. This we can do if there is a noetherian ring and a morphism which is proper. In this case, it is a nontrivial theorem that the cohomology groups of any coherent sheaf on are finitely generated -modules.
Grothendieck’s finiteness theorem is used to activate Artin-Rees lemma, which is used to show the image forms the -adic filtration on , and also the maps are eventually zero for where or .
To see this for , it essentially concerns showing that given an finite etale cover of , it can be extended to one over . The idea is that we can extend it to where is the -th order thinckening of , because etale sites are insensitive to nilpotent elements. Thus we get an etale cover of the formal scheme . According to the theorem of algebraisation of formal coherent sheaf (or Grothendieck’s existence theorem, see Stacks 088C, part of formal GAGA), is the formal completion of an etale cover of . We want to get back an etale cover over , and this is precisely what Artin’s approximatin theorem enables us to do (to use Artin approximation I think properness is not required, but it is essential for formal GAGA).
Reference:
https://virtualmath1.stanford.edu/~conrad/Weil2seminar/Notes/L6.pdf
https://stacks.math.columbia.edu/tag/095S