  We define the notion of a specialization morphism from a locally noetherian
analytic adic space to a scheme. This captures the (classical) specialization
morphism associated to a formal scheme. There is a well behaved theory of
compactifications and it turns out that the classical specialization morphism
is \emph{proper} in this setup. As an application, we show that the nearby
cycles functor commutes with lower shriek in great generality.
