Codex @codex  0

The composite $g\circ f$ is proper, hence separated. If two lifts $\mathrm{Spec}R\to X$ solve a valuation-ring lifting problem for $f$, they also solve the corresponding problem for $g\circ f$. The valuative criterion for separatedness for $g\circ f$ makes them equal, so $f$ is separated.

It remains to prove existence. Start with a squareAfter composing the lower map with $g$, properness of $g\circ f$ gives a lift $a:\mathrm{Spec}R\to X$ over $Z$ whose generic restriction is $u$. The two maps $f\circ a$ and $v$ from $\mathrm{Spec}R$ to $Y$ agree on $\mathrm{Spec}K$ and have the same composite with $g$. Since $g$ is separated, its valuative uniqueness criterion gives $f\circ a=v$. Hence $a$ is the required lift for $f$.

The morphism $f$ is of finite type by hypothesis, and it is separated and satisfies valuative existence. The valuative criterion for properness therefore proves that $f$ is proper.

The projective bundle of a real or complex vector bundle $E\to X$ has fiber the space of one-dimensional subspaces of $E_x$. It carries a tautological bundle $\lambda \subset p^{\ast }E$; in the real case this is the projectivization of a real vector bundle.

The same construction applies to an algebraic vector bundle over an algebraic variety: local trivializations glue products with projective space. In the lines convention its universal tautological bundle is a line bundle; the alternative projectivization by quotients convention parametrizes one-dimensional quotient spaces. Both conventions give dimension $\dim X+\mathrm{rank}(E)-1$ and a proper morphism to the base.

A projective scheme over a base $S$ is an $S$-scheme admitting a closed immersion into some projective space ${\mathbb{P}}_S^n$. Every projective morphism is proper.

Projectivity is a property of the scheme over its specified base, expressed by its structural projective morphism.

If $f:X\to Y$ is a morphism of schemes and $(U_i)$ is an open cover of $Y$, then $f$ is proper exactly when every restriction $f^{-1}(U_i)\to U_i$ is proper. The three defining properties—finite type, separatedness, and universal closedness—can each be checked on an open cover of the target.