nLab valuative criterion of properness

The valuative criterion of properness EGA II, 7.3.8 (numdam). It has been found by Chevalley.

Théorème (7.3.8). — Soient Y un préschéma (resp. un préschéma localement noethérien), $X\to Y$ un morphisme quasi-compact séparé (resp. de type fini). Les conditions suivantes sont équivalentes :

a) f est universellement fermé (resp. propre).

b) Pour tout $Y$-schéma de la forme $Y'=Spec(A)$, où $A$ est un anneau de valuation (resp. anneau de valuation discrète) de corps des fractions $K$, l’application canonique

$$Hom_Y(Y', X) \to Hom_Y(Spec(K), X)$$

correspondant à l’injection canonique $A\to K$, est surjective (resp. bijective).

In other words, the class of proper morphisms satisfies the unique right lifting property with respect to the class of morphisms $Spec K\to Spec R$ formally dual to the injections of valuation rings into their fields of fractions.

There is a pattern-terminological reinterpretation in Kontsevich-Rosenberg, Noncommutative spaces, 6.8.1:

Let $M_v'$ be the family of canonical injections of valuation rings to their fields of fractions, and let $M_v$ be its image in the category of functors $CRing\to Set$. Consider schemes as covariant presheaves on $CRing$. Then a morphism $f:X\to Y$ of schemes is separated iff it is formally $M_v$-unramified, universally closed iff it is formally $M_v$-smooth and proper iff it is formally $M_v$-étale (in the sense of KR 6.3).