Computing dimension of a smooth scheme I'm having trouble finding enough reference to show the following seemingly true statement.
Let $K$ be a local field with ring of integer $\mathcal{O}_K$. Assume that $X$ is a smooth $\mathcal{O}_K$-scheme such that $X_K$ has dimension $n$. Then $X$ has dimension $n+1$.
Could someone point me to some references to general statements that leads to this result ?
 A: Actually, I've just figured out that this is false for trivial reasons, since $X_K$ is smooth over $\mathcal{O}_K$. 
But (still assuming smoothness of $X$ over $\mathcal{O}_K$), one can prove that dim$X=$ dim$X_K$ if $X=X_K$, and dim$X=$ dim$X_K+1$ if $X\varsupsetneq X_K$.
Here is the small argument: 
Note that $X$ being smooth, it is in particular flat over $\mathcal{O}_K$, and hence $X_K$ is dense in $X$ (because if you think of the affine case, $X_K$ dense in $X$ just means that $\mathcal{O}_K[X]\to K[X]$ is injective, which is the case when $\mathcal{O}_K[X]$ is $\mathcal{O}_K$-flat). But also note that $X_K$ is open in $X$ (being the inverse image of the open (dense) point of Spec$\mathcal{O}_K$).
Now, it is a general topological argument that for $U$ open dense subset of $X$, we have dim$U\leq $ dim$X$. As it will be needed, I quickly recall the proof: let $\lbrace U\cap F_i \rbrace_{i=0,...,n}$ be a maximal chain of irreducible closed subsets (where $ F_i $ are closed in $ X $). Since $ \overline{U\cap F_i }^{X} $ is irreducible in $ X $ and $ \overline{U\cap F_i }^{X}\cap U = U\cap F_{i} $, we can assume that $ F_{i} $ is irreducible in $ X $, and hence $ \lbrace F_{i}\rbrace_{i=0,...,n} $ is a chain of irreducible closed sets in $ X $.
We continue as follow: note that in the proof of dim$U\leq $ dim$X$, the sets $ U\cap F_i $ were chosen to be dense in $ F_{i} $, the chain $ F_0\varsubsetneq F_1 \varsubsetneq ... \varsubsetneq F_n $ cannot be refined in $ X $. Also, since $ F_n $ contains $ U $ and $ U $ is dense, we have that $ F_n = X $. Hence, dim$ X $ = dim $ X_K+ $ dim $ F_0 $ (here, we use the fact that $ X $ is catenary, which is morally the case because any non-bestial ring is catenary, and the rings under consideration indeed are because $ \mathcal{O}_K $ is a regular local ring, hence Cohen-Macaulay, hence universally catenary). So there just remains to prove that dim$ F_0=0 $ if $ X_K=X $ and dim$ F_0=1 $ if $ X_K\varsubsetneq X $.
The first case is trivially true ($X=X_K$ implies dim$ X= $dim$ X_K $), hence assume $ X_K\varsubsetneq X $. This is equivalent to $ X_k\neq \emptyset $ (where $k=\mathcal{O}_K/(\pi)$ is the residue field). Hence, $ X_k $ has a closed point, say $ F_{-1} $. Now, by Hensel's lemma for smooth varieties, this closed point lift to a (non-closed) point of $ X $, call it $ F_0 $. This $ F_0 $ is a closed point in $ X_K $ of dimension $ 1 $ in $ X $, as wanted.  
