Lifting valuative squares over a separated target

Let f : X ⟶ Y be a morphism to a separated scheme, for instance an affine one, and let R be a valuation ring with fraction field K. To verify the existence part of the valuative criterion for f, one extends K-points of X to R-points. When the K-point comes from a ring map φ : A → K through some morphism Spec A ⟶ X, for instance an affine chart of X, it extends as soon as φ takes values in R: compose Spec R ⟶ Spec A with the chart. The resulting R-point lies over the given R-point of Y automatically, because both are morphisms Spec R ⟶ Y that agree on Spec K, and such morphisms are equal when Y is separated (the uniqueness part of the valuative criterion).

This reduces the valuative criterion for a scheme covered by affine charts to a statement about ring maps out of the chart rings, as in the proof that the projective line is universally closed.

Main results

• AlgebraicGeometry.ValuativeCommSq.hasLift_of_specMap_comp: a valuative square over a morphism to a separated scheme has a lift as soon as its K-point factors through some Spec A by a ring map A → K with image in R.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Theorem II.4.7.
• The Stacks Project, Tag 01KF, the valuative criterion for universal closedness.

theorem AlgebraicGeometry.ValuativeCommSq.hasLift_of_specMap_comp {X Y : Scheme} [Y.IsSeparated] {f : X ⟶ Y} (S : ValuativeCommSq f) {A : CommRingCat} (c : Spec A ⟶ X) (φ : A ⟶ ↧S.K) (hφ : CategoryTheory.CategoryStruct.comp (Spec.map φ) c = S.i₁) (hR : ∀ (a : ↑A), IsLocalization.IsInteger S.R ((CategoryTheory.ConcreteCategory.hom φ) a)) : ⋯.HasLift

A valuative square over a morphism to a separated scheme lifts once its K-point factors through R: if the K-point S.i₁ of X is Spec φ followed by a morphism Spec A ⟶ X, and φ : A ⟶ K takes values in the valuation ring R, then the square has a lift.