Algebraization isomorphism, formal existence, mod p

Question

Let $X$ be a smooth projective variety over a scheme $S$ being the spectrum of a discrete valuation ring of mixed characteristic $(0,p)$. Let $X_n$ be the respective thickenings of the reduced special fiber $X_1$. Then there is the following algebraization isomorphism: $$Pic(X)\xrightarrow{\sim} \varprojlim Pic(X_n).$$

How can one deduce this isomorphism from Grothendieck's formal existence theorem [EGA3, 5.1.4], saying that for a coherent $\mathcal{O}_X$-module $\mathcal{F}$, there is an isomorphism $$H^i(X,\mathcal{F})\rightarrow H^i(\hat{X},\hat{\mathcal{F}}),$$ where $\hat{X}$ is the formal scheme obtained by completing $X$ along $X_1$?

(The first idea that comes to my mind is considering $H^1$ and the module $\mathcal{O}_X^*$ - which might not be coherent? - but I don't understand the object on the right).

What are the problems if I want to consider $Pic(X_1)\otimes \mathbb{Z}/p\mathbb{Z}$, i.e. $p$ being the characteristic of the residue field of the base? Why does one have to consider thickenings instead? (this question could be put in a more general context, i.e. different cohomology theories mod $p$ in char $p$).

Answer 1

As you imply, you can identify $\varprojlim_n \mathrm{Pic}(X_n)$ with $\mathrm{Pic}(\hat{X})$, the Picard group of the completion of $X$, but think that you can deduce that the natural functor $\mathrm{Pic}(X)\rightarrow \mathrm{Pic}(\hat{X})$ is an equivalence from the theorem you state. What does follow is that the functor is fully faithful, since $$\mathrm{Hom}(\mathcal{L},\mathcal{M})\cong H^0(X,\mathcal{L}^\vee\otimes \mathcal{M}) \cong H^0(\hat{X},\hat{\mathcal{L}}^\vee\otimes \hat{\mathcal{M}})\cong \mathrm{Hom}(\hat{\mathcal{L}},\hat{\mathcal{M}})$$ but you need more than isomorphisms on cohomology to deduce essentially surjectivity. $\mathcal{O}_X^*$ is definitely not coherent (what's the $\mathcal{O}_X$-module structure?) so you can't apply the theorem.

Actually, the result you state is numbered as 5.1.2 in EGA3.1, and Theorem 5.1.4 on the next page is the result that the completion functor is an equivalence of categories between coherent modules on $X$ and those on $\hat{X}$. The proof there certainly doesn't follow straightforwardly from the isomorphism on cohomology, it goes by showing that every coherent sheaf is a quotient of a direct sum of (negative) powers of an ample line bundle.

So maybe I've misunderstood your question?