Rational maps into proper schemes from schemes with valuation rings as local rings

Let X be an integral S-scheme all of whose local rings are valuation rings, for instance a regular integral scheme of dimension one (a normal curve), and let Y be an S-scheme which is universally closed and locally of finite type over S. Then every S-rational map X ⤏ Y is defined everywhere (AlgebraicGeometry.Scheme.RationalMap.domain_eq_top_of_valuationRing).

At a point x of X, the rational map gives a morphism Spec K(X) ⟶ Y from the generic point, and 𝒪_{X,x} is a valuation ring with fraction field K(X). The existence part of the valuative criterion lifts this morphism to Spec 𝒪_{X,x} ⟶ Y, and the lift spreads out to a partial map defined at x which represents the same rational map.

When Y is moreover separated over a separated base, the rational map is a morphism. Together with Mathlib's correspondence between rational maps and morphisms from the generic point, this gives the extension theorem: every S-morphism Spec K(X) ⟶ Y extends uniquely to an S-morphism X ⟶ Y (AlgebraicGeometry.Scheme.homOfFunctionField). For curves this is the statement that a rational map from a normal curve to a proper scheme extends to a morphism, through which morphisms of normal proper curves are read off from embeddings of their function fields.

Main definitions

• AlgebraicGeometry.Scheme.RationalMap.toHom: a rational map from a reduced scheme to a separated scheme that is defined everywhere, as a morphism.
• AlgebraicGeometry.Scheme.homOfFunctionField: the morphism X ⟶ Y extending an S-morphism Spec K(X) ⟶ Y.

Main results

• AlgebraicGeometry.Scheme.RationalMap.domain_eq_top_of_valuationRing: an S-rational map from an integral scheme whose local rings are valuation rings to a universally closed S-scheme locally of finite type is defined everywhere.
• AlgebraicGeometry.Scheme.fromSpecStalk_homOfFunctionField and AlgebraicGeometry.Scheme.eq_homOfFunctionField_iff: homOfFunctionField extends the given morphism, and is the only S-morphism that does.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Proposition I.6.8 (the case of a nonsingular curve and a projective variety) and Theorem II.4.7 (the valuative criterion).

theorem AlgebraicGeometry.Scheme.Opens.SpecMap_stalkSpecializes_fromSpecStalkOfMem {X : Scheme} (U : X.Opens) {x y : ↥X} (h : y ⤳ x) (hx : x ∈ U) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.stalkSpecializes h)) (U.fromSpecStalkOfMem x hx) = U.fromSpecStalkOfMem y ⋯

The canonical morphisms from the spectra of stalks into an open subscheme are compatible with generization: for a generization y of a point x of U, the morphism Spec 𝒪_{X,y} ⟶ U is the morphism Spec 𝒪_{X,x} ⟶ U precomposed with Spec of the specialization map.

theorem AlgebraicGeometry.Scheme.Opens.SpecMap_stalkSpecializes_fromSpecStalkOfMem_assoc {X : Scheme} (U : X.Opens) {x y : ↥X} (h : y ⤳ x) (hx : x ∈ U) {Z : Scheme} (h✝ : ↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.stalkSpecializes h)) (CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hx) h✝) = CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem y ⋯) h✝

The canonical morphisms from the spectra of stalks into an open subscheme are compatible with generization: for a generization y of a point x of U, the morphism Spec 𝒪_{X,y} ⟶ U is the morphism Spec 𝒪_{X,x} ⟶ U precomposed with Spec of the specialization map.

theorem AlgebraicGeometry.Scheme.PartialMap.SpecMap_stalkSpecializes_fromSpecStalkOfMem {X Y : Scheme} [IrreducibleSpace ↥X] (g : X.PartialMap Y) {x : ↥X} (hx : x ∈ g.domain) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.stalkSpecializes ⋯)) (g.fromSpecStalkOfMem hx) = g.fromFunctionField

The morphism Spec K(X) ⟶ Y of a partial map is its morphism Spec 𝒪_{X,x} ⟶ Y at any point x of its domain, precomposed with Spec of the specialization map from the generic point.

theorem AlgebraicGeometry.Scheme.PartialMap.SpecMap_stalkSpecializes_fromSpecStalkOfMem_assoc {X Y : Scheme} [IrreducibleSpace ↥X] (g : X.PartialMap Y) {x : ↥X} (hx : x ∈ g.domain) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (X.presheaf.stalkSpecializes ⋯)) (CategoryTheory.CategoryStruct.comp (g.fromSpecStalkOfMem hx) h) = CategoryTheory.CategoryStruct.comp g.fromFunctionField h

The morphism Spec K(X) ⟶ Y of a partial map is its morphism Spec 𝒪_{X,x} ⟶ Y at any point x of its domain, precomposed with Spec of the specialization map from the generic point.

Rational maps defined everywhere

theorem AlgebraicGeometry.Scheme.RationalMap.toPartialMap_domain {X Y : Scheme} [IsReduced X] [Y.IsSeparated] (f : X.RationalMap Y) : f.toPartialMap.domain = f.domain

The domain of the representative RationalMap.toPartialMap is the domain of definition.

noncomputable def AlgebraicGeometry.Scheme.RationalMap.toHom {X Y : Scheme} [IsReduced X] [Y.IsSeparated] (f : X.RationalMap Y) (hf : f.domain = ⊤) : X ⟶ Y

A rational map from a reduced scheme to a separated scheme which is defined everywhere, as a morphism: its representative on its domain of definition ⊤.

theorem AlgebraicGeometry.Scheme.RationalMap.fromSpecStalk_toHom {X Y : Scheme} [IsReduced X] [Y.IsSeparated] (f : X.RationalMap Y) (hf : f.domain = ⊤) (x : ↥X) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (f.toHom hf) = f.toPartialMap.fromSpecStalkOfMem ⋯

On the spectrum of the stalk at a point, RationalMap.toHom is the representative of the rational map on its domain of definition.

theorem AlgebraicGeometry.Scheme.RationalMap.fromSpecStalk_toHom_assoc {X Y : Scheme} [IsReduced X] [Y.IsSeparated] (f : X.RationalMap Y) (hf : f.domain = ⊤) (x : ↥X) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) (CategoryTheory.CategoryStruct.comp (f.toHom hf) h) = CategoryTheory.CategoryStruct.comp (f.toPartialMap.fromSpecStalkOfMem ⋯) h

On the spectrum of the stalk at a point, RationalMap.toHom is the representative of the rational map on its domain of definition.

theorem AlgebraicGeometry.Scheme.RationalMap.fromSpecStalk_genericPoint_toHom {X Y : Scheme} [IsIntegral X] [Y.IsSeparated] (f : X.RationalMap Y) (hf : f.domain = ⊤) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (f.toHom hf) = f.fromFunctionField

At the generic point, RationalMap.toHom is the morphism Spec K(X) ⟶ Y of the rational map.

theorem AlgebraicGeometry.Scheme.RationalMap.fromSpecStalk_genericPoint_toHom_assoc {X Y : Scheme} [IsIntegral X] [Y.IsSeparated] (f : X.RationalMap Y) (hf : f.domain = ⊤) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (CategoryTheory.CategoryStruct.comp (f.toHom hf) h) = CategoryTheory.CategoryStruct.comp f.fromFunctionField h

At the generic point, RationalMap.toHom is the morphism Spec K(X) ⟶ Y of the rational map.

@[simp]

theorem AlgebraicGeometry.Scheme.RationalMap.toRationalMap_toHom {X Y : Scheme} [IsIntegral X] [Y.IsSeparated] (f : X.RationalMap Y) (hf : f.domain = ⊤) : Hom.toRationalMap (f.toHom hf) = f

The morphism RationalMap.toHom represents the rational map.

Rational maps into universally closed schemes

theorem AlgebraicGeometry.Scheme.RationalMap.domain_ofFunctionField_eq_top {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (φ : Spec X.functionField ⟶ Y) (hφ : CategoryTheory.CategoryStruct.comp φ (Y ↘ S) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ S)) : (ofFunctionField (X ↘ S) (Y ↘ S) φ hφ).domain = ⊤

Rational maps from schemes with valuation rings as local rings into universally closed schemes are defined everywhere, in the form of the rational map spread out from an S-morphism φ : Spec K(X) ⟶ Y. At a point x, the valuative criterion lifts φ to Spec 𝒪_{X,x}, and the lift spreads out to a partial map defined at x.

theorem AlgebraicGeometry.Scheme.RationalMap.domain_eq_top_of_valuationRing {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (f : X.RationalMap Y) [IsOver S f] : f.domain = ⊤

Rational maps from schemes with valuation rings as local rings into universally closed schemes are defined everywhere: let X be an integral S-scheme whose local rings are valuation rings (for instance a normal curve) and Y an S-scheme universally closed and locally of finite type over S. Then every S-rational map X ⤏ Y is defined at every point of X.

Extending morphisms from the generic point

noncomputable def AlgebraicGeometry.Scheme.homOfFunctionField {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [S.IsSeparated] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] [IsSeparated (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (φ : Spec X.functionField ⟶ Y) (hφ : CategoryTheory.CategoryStruct.comp φ (Y ↘ S) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ S)) : X ⟶ Y

A morphism from the generic point extends to the whole scheme: for an integral S-scheme X whose local rings are valuation rings and an S-scheme Y universally closed, locally of finite type and separated over a separated base S (for instance proper over S), the S-morphism X ⟶ Y extending an S-morphism φ : Spec K(X) ⟶ Y (fromSpecStalk_homOfFunctionField), which is unique (eq_homOfFunctionField_iff).

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecStalk_homOfFunctionField {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [S.IsSeparated] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] [IsSeparated (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (φ : Spec X.functionField ⟶ Y) (hφ : CategoryTheory.CategoryStruct.comp φ (Y ↘ S) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ S)) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (homOfFunctionField hX φ hφ) = φ

homOfFunctionField extends the morphism from the generic point.

@[simp]

theorem AlgebraicGeometry.Scheme.fromSpecStalk_homOfFunctionField_assoc {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [S.IsSeparated] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] [IsSeparated (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (φ : Spec X.functionField ⟶ Y) (hφ : CategoryTheory.CategoryStruct.comp φ (Y ↘ S) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ S)) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (CategoryTheory.CategoryStruct.comp (homOfFunctionField hX φ hφ) h) = CategoryTheory.CategoryStruct.comp φ h

homOfFunctionField extends the morphism from the generic point.

instance AlgebraicGeometry.Scheme.isOver_homOfFunctionField {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [S.IsSeparated] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] [IsSeparated (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (φ : Spec X.functionField ⟶ Y) (hφ : CategoryTheory.CategoryStruct.comp φ (Y ↘ S) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ S)) : Hom.IsOver (homOfFunctionField hX φ hφ) S

homOfFunctionField is a morphism over S.

theorem AlgebraicGeometry.Scheme.eq_homOfFunctionField_iff {X Y S : Scheme} [X.Over S] [Y.Over S] [IsIntegral X] [S.IsSeparated] [UniversallyClosed (Y ↘ S)] [LocallyOfFiniteType (Y ↘ S)] [IsSeparated (Y ↘ S)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (φ : Spec X.functionField ⟶ Y) (hφ : CategoryTheory.CategoryStruct.comp φ (Y ↘ S) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (X ↘ S)) (f : X ⟶ Y) [Hom.IsOver f S] : f = homOfFunctionField hX φ hφ ↔ CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) f = φ

The extension of a morphism from the generic point is unique: an S-morphism X ⟶ Y is homOfFunctionField hX φ hφ exactly when it restricts to φ on the generic point.