I am little confused about properness for schemes.
Let $X \rightarrow \operatorname{Spec}(k)$ be a proper morphism. If $K/k$ is a field extension, then $X_K= X \times_k K \rightarrow \operatorname{Spec}(K)$ is proper.
But what about the morphism $X_K \rightarrow X$ ? Is it also proper? Or are some conditions needed to get properness?
This happens exactly when $K/k$ is a finite extension.
One direction is clear: if $K/k$ is finite, then $\operatorname{Spec} K\to \operatorname{Spec} k$ is proper, and as properness is preserved under base change, $X_K\to X$ is proper.
For the other direction, here's something that's potentially overkill but has the advantage of turning this in to a one-liner: as properness descends along fpqc morphisms (EGA IV2, 2.7.1(vii)), $X_K\to X$ proper implies $\operatorname{Spec} K\to \operatorname{Spec} k$ is proper. But any morphism which is both proper and affine is finite.
Alternately, per a suggestion of Alex Youcis in the comments, $X$ proper over $k$ implies that $\mathcal{O}_X(X)$ is finite over $k$. So if $X_K$ is proper over $X$, then $X_K$ is proper over $k$ and $\mathcal{O}_{X_K}(X_K)$ must be finite over $k$. But $\mathcal{O}_{X_K}(X_K)$ contains a copy of $K$, and therefore $K$ must be finite over $k$.