Morphisms into proper schemes from maps of function fields

Let k be a commutative ring, X an integral k-scheme all of whose local rings are valuation rings (for instance a regular integral scheme of dimension one, a normal curve), and Y an integral k-scheme proper over k. Every k-algebra map ψ : k(Y) → k(X) of function fields is the pullback of rational functions along a unique dominant k-morphism X ⟶ Y (AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom): Spec ψ moves the generic point of X into Y, and this morphism Spec k(X) ⟶ Y extends to all of X (AlgebraicGeometry.Scheme.homOfFunctionField).

The construction is functorial, so when X and Y both have valuation rings as local rings and are both proper over k, a k-isomorphism of their function fields gives an isomorphism of k-schemes (AlgebraicGeometry.Scheme.isoOfFunctionFieldAlgEquiv). For curves over a field this says that a regular proper curve is determined by its function field: proper normal curves which are birational are isomorphic.

Main definitions

• AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom: the dominant k-morphism X ⟶ Y whose pullback of rational functions is a given k-algebra map k(Y) → k(X).
• AlgebraicGeometry.Scheme.isoOfFunctionFieldAlgEquiv: the isomorphism X ≅ Y induced by a k-isomorphism k(Y) ≃ k(X).

Main results

• AlgebraicGeometry.Scheme.functionFieldMap_homOfFunctionFieldAlgHom: the pullback of rational functions along homOfFunctionFieldAlgHom hX ψ is ψ.
• AlgebraicGeometry.Scheme.eq_homOfFunctionFieldAlgHom_iff: a dominant k-morphism is homOfFunctionFieldAlgHom hX ψ exactly when its pullback of rational functions is ψ.
• AlgebraicGeometry.Scheme.functionFieldAlgHom_homOfFunctionFieldAlgHom and AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_functionFieldAlgHom: the construction is inverse to the pullback of rational functions AlgebraicGeometry.Scheme.Hom.functionFieldAlgHom.
• AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_id and AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_comp: functoriality.

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Proposition I.6.8 and Corollary I.6.12.

noncomputable def AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) : X ⟶ Y

The morphism induced by a map of function fields: for an integral k-scheme X whose local rings are valuation rings and an integral k-scheme Y proper over k, the unique dominant k-morphism X ⟶ Y whose pullback of rational functions is the k-algebra map ψ : k(Y) → k(X) (functionFieldMap_homOfFunctionFieldAlgHom, eq_homOfFunctionFieldAlgHom_iff).

theorem AlgebraicGeometry.Scheme.fromSpecStalk_homOfFunctionFieldAlgHom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (homOfFunctionFieldAlgHom hX ψ) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom ψ.toRingHom)) (Y.fromSpecStalk (genericPoint ↥Y))

On the generic point, homOfFunctionFieldAlgHom hX ψ is Spec ψ.

theorem AlgebraicGeometry.Scheme.fromSpecStalk_homOfFunctionFieldAlgHom_assoc {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (CategoryTheory.CategoryStruct.comp (homOfFunctionFieldAlgHom hX ψ) h) = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom ψ.toRingHom)) (CategoryTheory.CategoryStruct.comp (Y.fromSpecStalk (genericPoint ↥Y)) h)

On the generic point, homOfFunctionFieldAlgHom hX ψ is Spec ψ.

instance AlgebraicGeometry.Scheme.instIsOverHomOfFunctionFieldAlgHomSpecOf {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) : Hom.IsOver (homOfFunctionFieldAlgHom hX ψ) (Spec ↧k)

homOfFunctionFieldAlgHom hX ψ is a morphism over k.

instance AlgebraicGeometry.Scheme.instIsDominantHomOfFunctionFieldAlgHom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) : IsDominant (homOfFunctionFieldAlgHom hX ψ)

homOfFunctionFieldAlgHom hX ψ is dominant: it sends the generic point to the generic point.

@[simp]

theorem AlgebraicGeometry.Scheme.functionFieldMap_homOfFunctionFieldAlgHom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) : Hom.functionFieldMap (homOfFunctionFieldAlgHom hX ψ) = CommRingCat.ofHom ψ.toRingHom

The pullback of rational functions along homOfFunctionFieldAlgHom hX ψ is ψ.

theorem AlgebraicGeometry.Scheme.eq_homOfFunctionFieldAlgHom_iff {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) (f : X ⟶ Y) [Hom.IsOver f (Spec ↧k)] [IsDominant f] : f = homOfFunctionFieldAlgHom hX ψ ↔ ∀ (a : ↑Y.functionField), (CategoryTheory.ConcreteCategory.hom (Hom.functionFieldMap f)) a = ψ a

A dominant morphism into a proper scheme is determined by its pullback of rational functions: a dominant k-morphism f : X ⟶ Y is homOfFunctionFieldAlgHom hX ψ exactly when its pullback of rational functions is ψ.

@[simp]

theorem AlgebraicGeometry.Scheme.functionFieldAlgHom_homOfFunctionFieldAlgHom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) : Hom.functionFieldAlgHom k (homOfFunctionFieldAlgHom hX ψ) = ψ

The pullback of rational functions along homOfFunctionFieldAlgHom hX ψ is ψ, as a k-algebra map.

@[simp]

theorem AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_functionFieldAlgHom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (f : X ⟶ Y) [Hom.IsOver f (Spec ↧k)] [IsDominant f] : homOfFunctionFieldAlgHom hX (Hom.functionFieldAlgHom k f) = f

A dominant morphism into a proper scheme is induced by its pullback of rational functions: a dominant k-morphism f : X ⟶ Y is homOfFunctionFieldAlgHom of f^* : k(Y) → k(X).

Functoriality

@[simp]

theorem AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_id {k : Type u} [CommRing k] {X : Scheme} [X.Over (Spec ↧k)] [IsIntegral X] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) [IsProper (X ↘ Spec ↧k)] : homOfFunctionFieldAlgHom hX (AlgHom.id k ↑X.functionField) = CategoryTheory.CategoryStruct.id X

The identity of k(X) induces the identity of X.

theorem AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_comp {k : Type u} [CommRing k] {X Y Z : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [Z.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsIntegral Z] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) [IsProper (Z ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (ψ' : ↑Z.functionField →ₐ[k] ↑Y.functionField) : CategoryTheory.CategoryStruct.comp (homOfFunctionFieldAlgHom hX ψ) (homOfFunctionFieldAlgHom hY ψ') = homOfFunctionFieldAlgHom hX (ψ.comp ψ')

k-algebra maps k(Z) → k(Y) → k(X) induce the composite X ⟶ Y ⟶ Z.

theorem AlgebraicGeometry.Scheme.homOfFunctionFieldAlgHom_comp_assoc {k : Type u} [CommRing k] {X Y Z : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [Z.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsIntegral Z] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) (ψ : ↑Y.functionField →ₐ[k] ↑X.functionField) [IsProper (Z ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (ψ' : ↑Z.functionField →ₐ[k] ↑Y.functionField) {Z✝ : Scheme} (h : Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (homOfFunctionFieldAlgHom hX ψ) (CategoryTheory.CategoryStruct.comp (homOfFunctionFieldAlgHom hY ψ') h) = CategoryTheory.CategoryStruct.comp (homOfFunctionFieldAlgHom hX (ψ.comp ψ')) h

k-algebra maps k(Z) → k(Y) → k(X) induce the composite X ⟶ Y ⟶ Z.

noncomputable def AlgebraicGeometry.Scheme.isoOfFunctionFieldAlgEquiv {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) [IsProper (X ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (e : ↑Y.functionField ≃ₐ[k] ↑X.functionField) : X ≅ Y

Proper schemes with valuation rings as local rings are determined by their function fields: for integral k-schemes X and Y, both proper over k and with valuation rings as local rings, the isomorphism X ≅ Y of k-schemes induced by a k-isomorphism e : k(Y) ≃ k(X) of function fields.

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfFunctionFieldAlgEquiv_hom {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) [IsProper (X ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (e : ↑Y.functionField ≃ₐ[k] ↑X.functionField) : (isoOfFunctionFieldAlgEquiv hX hY e).hom = homOfFunctionFieldAlgHom hX ↑e

The forward morphism of isoOfFunctionFieldAlgEquiv hX hY e is the morphism induced by e.

@[simp]

theorem AlgebraicGeometry.Scheme.isoOfFunctionFieldAlgEquiv_inv {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) [IsProper (X ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (e : ↑Y.functionField ≃ₐ[k] ↑X.functionField) : (isoOfFunctionFieldAlgEquiv hX hY e).inv = homOfFunctionFieldAlgHom hY ↑e.symm

The inverse morphism of isoOfFunctionFieldAlgEquiv hX hY e is the morphism induced by e.symm.

instance AlgebraicGeometry.Scheme.instIsOverHomIsoOfFunctionFieldAlgEquivSpecOf {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) [IsProper (X ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (e : ↑Y.functionField ≃ₐ[k] ↑X.functionField) : Hom.IsOver (isoOfFunctionFieldAlgEquiv hX hY e).hom (Spec ↧k)

isoOfFunctionFieldAlgEquiv hX hY e is a morphism over k.

instance AlgebraicGeometry.Scheme.instIsOverInvIsoOfFunctionFieldAlgEquivSpecOf {k : Type u} [CommRing k] {X Y : Scheme} [X.Over (Spec ↧k)] [Y.Over (Spec ↧k)] [IsIntegral X] [IsIntegral Y] [IsProper (Y ↘ Spec ↧k)] (hX : ∀ (x : ↥X), ValuationRing ↑(X.presheaf.stalk x)) [IsProper (X ↘ Spec ↧k)] (hY : ∀ (y : ↥Y), ValuationRing ↑(Y.presheaf.stalk y)) (e : ↑Y.functionField ≃ₐ[k] ↑X.functionField) : Hom.IsOver (isoOfFunctionFieldAlgEquiv hX hY e).inv (Spec ↧k)

The inverse of isoOfFunctionFieldAlgEquiv hX hY e is a morphism over k.