Definition of $p$-adic formal scheme Could someone please provide a precise definition of a $p$-adic formal scheme $X$ over a ring $A$?  Is it a formal scheme over $A$ which is locally isomorphic to $\operatorname{Spf}(B)$, where the completion is taken with respect to the ideal $(p) \subset B$?
Moreover, is there a relation to schemes over $p$-adic fields or rings?  e.g. can one embed $\mathbb{Z}_p$-schemes fully faithfully in $p$-adic formal schemes?
 A: To answer your first question, yes. An equivalent way of saying it, but one which may be more commonly said, is the following. Recall that a morphism $f\colon \mathfrak{X}\to\mathfrak{Y}$ of formal schemes is called adic if for one (equiv.) for all affine open covers $\{\mathrm{Spf}(A_i)\}$ of $\mathfrak{Y}$ and open covers $\{\mathrm{Spf}(B_{ij})\}$ of $f^{-1}(\mathrm{Spf}(A_i))$ the induced maps $A_i\to B_{ij}$ are adic:  for one (equiv. for all) ideals of definition $I$ of $A_i$, the ideal $IB_{ij}$ is an ideal of definition of $B_{ij}$. Then, a $p$-adic formal scheme means a formal scheme $\mathfrak{X}$ together with (a necessarily unique) adic morphism $\mathfrak{X}\to\mathrm{Spf}(\mathbf{Z}_p)$.
For any scheme $X\to\mathrm{Spec}(\mathbf{Z}_p)$ one may form the $p$-adic completion $\widehat{X}\to\mathrm{Spf}(\mathbf{Z}_p)$ which is obtained as the colimit of topologically locally ringed spaces${}^{\color{red}{(1)}}$
$$\varinjlim \,\,X_{\mathbf{Z}/p^n\mathbf{Z}_p}=\varinjlim \,\,(|X_{\mathbf{F}_p}|,\mathcal{O}_X/p^n\mathcal{O}_X),$$
which is a $p$-adic formal scheme. More concretely, writing
$$X=\mathrm{colim}\,\, \mathrm{Spec}(A)$$
(see this) one has that
$$\widehat{X}=\mathrm{colim}\,\, \mathrm{Spf}(\widehat{A}),$$
where $\widehat{A}:=\varprojlim A/p^nA$ is the $p$-adic completion of $A$ (which is functorial in $A$).
This gives us a functor
$$\widehat{(-)}\colon\left\{\begin{matrix}\text{Schemes over }\\ \mathbf{Z}_p\end{matrix}\right\}\to \left\{\begin{matrix}p\text{-adic formal }\\ \text{schemes}\end{matrix}\right\},$$
but this functor is far from fully faithful:

*

*the $p$-adic completion of $\mathrm{Spec}(\mathbf{Q}_p)$ is empty: $\mathbf{Q}_p/p^n\mathbf{Q}_p=0$ for all $n\geqslant 1$,

*a less trivial example is giving by observing that $\mathbf{A}^1_{\mathbf{Z}_p}$ and $\mathrm{Spec}(\mathbf{Z}_p[x,(1-px)^{-1}])$ give non-isomorphic decompletions of $\mathrm{Spf}(\mathbf{Z}_p\langle x\rangle)$(where $\mathbf{Z}_p\langle x\rangle$ is the set of $p$-adically convergent power series with coefficients in $\mathbf{Z}_p$).${}^{\color{red}{(2)}}$
That said, there are two significant subcategories of $\mathbf{Z}_p$-schemes for which the $p$-adic completion functor is fully faithful:

*

*$\mathbf{F}_p$-schemes (there the $p$-adic completion functor is the identity!),

*the category of proper $\mathbf{Z}_p$-schemes: this is a '$p$-adic GAGA theorem' (e.g. see [FK, Chapter I, Proposition 10.3.1] for a very general statement).

$\color{red}{(1)}$: there is a small subtelty when $X$ is not topologically Noetherian -- in this case you need to take this limit of the sheaves $\varprojlim \mathcal{O}_X/p^n\mathcal{O}_X$ in the category of sheaves of topological ring where each $\mathcal{O}_X/p^n\mathcal{O}_X$ is given the pseudo-discrete topology (e.g. see this).
$\color{red}{(2)}$: Indeed, these schemes are evidently non-isomorphic, as we have functorial identifications
$$\mathrm{Hom}(\mathrm{Spec}(R),\mathbf{A}^1_{\mathbf{Z}_p})=R,$$
$$\mathrm{Hom}(\mathrm{Spec}(R),\mathrm{Spec}(\mathbf{Z}_p[x,(1-px)^{-1}]))=\{x\in R: 1-px\in R^\times\}.$$
That said, their completions are isomorphic as their moduli problems are given by
$$\mathrm{Hom}(\mathrm{Spf}(A),\hat{\mathbf{A}}^1_{\mathbf{Z}_p})=A,$$
$$\mathrm{Hom}(\mathrm{Spf}(A),\mathrm{Spec}(\mathbf{Z}_p[x,(1-px)^{-1}])^{\wedge})=\{x\in A: 1-px\in A^\times\},$$
but as $A$ is $p$-adically complete we know that $1-px$ is automatically invertible for any $x\in A$ (e.g. see [FK, Chapter 0, Lemma 7.2.13]).
References:
[FK] Fujiwara, K. and Kato, F., 2018. Foundations of rigid geometry. European Mathematical Society.
