Dominant morphisms and rational functions

A morphism f : X ⟶ Y of schemes is dominant (AlgebraicGeometry.IsDominant) when its image is dense. Between irreducible schemes this says exactly that f sends the generic point of X to the generic point of Y. The map of stalks at the generic point is then a homomorphism f^* : K(Y) ⟶ K(X) of generic stalks, the pullback of rational functions along f. (The generic stalk K(X) of an irreducible scheme is a local ring; it is the function field, a field, when X is integral.) It is the homomorphism through which f acts on the generic point: the canonical morphism Spec K(X) ⟶ X followed by f is Spec f^* followed by the canonical morphism Spec K(Y) ⟶ Y, and f^* is the only homomorphism with this property.

This is how a dominant morphism of integral curves is compared with a homomorphism of function fields given by other means, for instance by explicit formulae: it suffices to compute the image of the generic point. Into a separated target nothing more is needed: the generic point is dense in a reduced irreducible scheme, so a morphism into a separated scheme is determined by what it does to the generic point, and a dominant one by its pullback of rational functions.

Main definitions

• AlgebraicGeometry.Scheme.Hom.functionFieldMap: the pullback K(Y) ⟶ K(X) of rational functions along a dominant morphism f : X ⟶ Y of irreducible schemes.

Main results

• AlgebraicGeometry.IsDominant.pullback_fst_of_isOpenMap: base change of a dominant morphism along a morphism with open underlying map (for instance an étale morphism) is dominant, without reducedness or irreducibility assumptions.
• AlgebraicGeometry.Scheme.Hom.genericPoint_eq_of_isDominant: a dominant morphism of irreducible schemes sends the generic point to the generic point.
• AlgebraicGeometry.isDominant_iff_genericPoint_eq: conversely, a morphism of irreducible schemes sending the generic point to the generic point is dominant.
• AlgebraicGeometry.Scheme.Hom.isDominant_of_SpecMap_fromSpecStalk: a morphism of irreducible schemes whose action on the generic point is given by a homomorphism of generic stalks is dominant.
• AlgebraicGeometry.Scheme.Hom.SpecMap_functionFieldMap_fromSpecStalk: Spec f^* followed by Spec K(Y) ⟶ Y is Spec K(X) ⟶ X followed by f.
• AlgebraicGeometry.Scheme.Hom.eq_functionFieldMap_iff: f^* is the only homomorphism of generic stalks with this property.
• AlgebraicGeometry.Scheme.Hom.germToFunctionField_functionFieldMap: f^* sends the germ of a section s over an open U to the germ of its pullback f^* s over f⁻¹ U.
• AlgebraicGeometry.Scheme.Hom.functionFieldMap_algebraMap_stalk: f^* is compatible with the maps of stalks 𝒪_{Y,f x} ⟶ 𝒪_{X,x}.
• AlgebraicGeometry.Scheme.Hom.appLE_injective_of_isDominant: from an irreducible scheme to an integral scheme, the pullback of sections Γ(Y, U) ⟶ Γ(X, V) along a dominant morphism is injective for nonempty V.
• AlgebraicGeometry.Scheme.Hom.functionFieldMap_id and AlgebraicGeometry.Scheme.Hom.functionFieldMap_comp: functoriality.
• AlgebraicGeometry.isDominant_fromSpecStalk_genericPoint: the canonical morphism Spec K(X) ⟶ X is dominant.
• AlgebraicGeometry.Scheme.Hom.ext_of_functionFieldMap_eq: dominant morphisms from a reduced irreducible scheme to a separated scheme agree as soon as their pullbacks of rational functions agree.

References

• [R. Hartshorne, Algebraic Geometry][hartshorne1977], Chapter I, Theorem 4.4 (dominant rational maps of varieties and homomorphisms of function fields).

theorem AlgebraicGeometry.IsDominant.pullback_fst_of_isOpenMap {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsDominant g] (hf : IsOpenMap ⇑f) : IsDominant (CategoryTheory.Limits.pullback.fst f g)

Base change of a dominant morphism along a morphism whose underlying map is open is dominant. No flatness or reducedness assumption is needed.

theorem AlgebraicGeometry.Scheme.Hom.irreducibleSpace_of_isDominant {X Y : Scheme} [IrreducibleSpace ↥X] (f : X ⟶ Y) [IsDominant f] : IrreducibleSpace ↥Y

The target of a dominant morphism from an irreducible scheme is irreducible.

instance AlgebraicGeometry.Scheme.Hom.nonempty_preimage_of_isDominant {X Y : Scheme} (f : X ⟶ Y) [IsDominant f] (U : Y.Opens) [Nonempty ↥↑U] : Nonempty ↥↑((TopologicalSpace.Opens.map f.base).obj U)

The preimage of a nonempty open under a dominant morphism is nonempty.

theorem AlgebraicGeometry.Scheme.Hom.genericPoint_eq_of_isDominant {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] : f (genericPoint ↥X) = genericPoint ↥Y

A dominant morphism of irreducible schemes sends the generic point to the generic point.

theorem AlgebraicGeometry.isDominant_iff_genericPoint_eq {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] {f : X ⟶ Y} : IsDominant f ↔ f (genericPoint ↥X) = genericPoint ↥Y

A morphism of irreducible schemes is dominant exactly when it sends the generic point to the generic point.

instance AlgebraicGeometry.isDominant_fromSpecStalk_genericPoint {X : Scheme} [IrreducibleSpace ↥X] : IsDominant (X.fromSpecStalk (genericPoint ↥X))

The canonical morphism Spec K(X) ⟶ X from the spectrum of the generic stalk of an irreducible scheme is dominant: its image is the generic point, which is dense.

theorem AlgebraicGeometry.Scheme.Hom.isDominant_of_SpecMap_fromSpecStalk {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) (φ : Y.functionField ⟶ X.functionField) (h : CategoryTheory.CategoryStruct.comp (Spec.map φ) (Y.fromSpecStalk (genericPoint ↥Y)) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) f) : IsDominant f

A morphism f : X ⟶ Y of irreducible schemes is dominant when the canonical morphism Spec K(X) ⟶ X followed by f factors as Spec φ followed by the canonical morphism Spec K(Y) ⟶ Y, for a homomorphism φ : K(Y) ⟶ K(X) of generic stalks (function fields when X and Y are integral). The homomorphism φ need not be local, since the spectrum of the generic stalk of Y has a single point, which maps to the generic point. It is then the pullback of rational functions along f (Scheme.Hom.eq_functionFieldMap_iff).

noncomputable def AlgebraicGeometry.Scheme.Hom.functionFieldMap {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] : Y.functionField ⟶ X.functionField

The pullback of rational functions f^* : K(Y) ⟶ K(X) along a dominant morphism f : X ⟶ Y of irreducible schemes: the map of stalks of f at the generic point of X, which f sends to the generic point of Y (genericPoint_eq_of_isDominant). It is characterised by SpecMap_functionFieldMap_fromSpecStalk and eq_functionFieldMap_iff, and it sends the germ of a section s to the germ of f^* s (germToFunctionField_functionFieldMap).

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.SpecMap_functionFieldMap_fromSpecStalk {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] : CategoryTheory.CategoryStruct.comp (Spec.map (functionFieldMap f)) (Y.fromSpecStalk (genericPoint ↥Y)) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) f

The pullback of rational functions describes the image of the generic point: for a dominant morphism f : X ⟶ Y of irreducible schemes, the canonical morphism Spec K(X) ⟶ X followed by f is Spec f^* followed by the canonical morphism Spec K(Y) ⟶ Y.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.SpecMap_functionFieldMap_fromSpecStalk_assoc {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (Spec.map (functionFieldMap f)) (CategoryTheory.CategoryStruct.comp (Y.fromSpecStalk (genericPoint ↥Y)) h) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) (CategoryTheory.CategoryStruct.comp f h)

The pullback of rational functions describes the image of the generic point: for a dominant morphism f : X ⟶ Y of irreducible schemes, the canonical morphism Spec K(X) ⟶ X followed by f is Spec f^* followed by the canonical morphism Spec K(Y) ⟶ Y.

theorem AlgebraicGeometry.Scheme.Hom.eq_functionFieldMap_iff {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] (φ : Y.functionField ⟶ X.functionField) : φ = functionFieldMap f ↔ CategoryTheory.CategoryStruct.comp (Spec.map φ) (Y.fromSpecStalk (genericPoint ↥Y)) = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) f

The pullback of rational functions is unique: a homomorphism φ : K(Y) ⟶ K(X) of generic stalks (function fields when X and Y are integral) is the pullback f^* along a dominant morphism f : X ⟶ Y of irreducible schemes exactly when Spec φ followed by the canonical morphism Spec K(Y) ⟶ Y is the canonical morphism Spec K(X) ⟶ X followed by f.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.germToFunctionField_functionFieldMap {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] (U : Y.Opens) [Nonempty ↥↑U] : CategoryTheory.CategoryStruct.comp (Y.germToFunctionField U) (functionFieldMap f) = CategoryTheory.CategoryStruct.comp (app f U) (X.germToFunctionField ((TopologicalSpace.Opens.map f.base).obj U))

The pullback of rational functions f^* along a dominant morphism f : X ⟶ Y of irreducible schemes sends the germ at the generic point of a section s of 𝒪_Y over a nonempty open U to the germ of its pullback f^* s over f⁻¹ U.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.germToFunctionField_functionFieldMap_assoc {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] (U : Y.Opens) [Nonempty ↥↑U] {Z : CommRingCat} (h : X.functionField ⟶ Z) : CategoryTheory.CategoryStruct.comp (Y.germToFunctionField U) (CategoryTheory.CategoryStruct.comp (functionFieldMap f) h) = CategoryTheory.CategoryStruct.comp (app f U) (CategoryTheory.CategoryStruct.comp (X.germToFunctionField ((TopologicalSpace.Opens.map f.base).obj U)) h)

The pullback of rational functions f^* along a dominant morphism f : X ⟶ Y of irreducible schemes sends the germ at the generic point of a section s of 𝒪_Y over a nonempty open U to the germ of its pullback f^* s over f⁻¹ U.

theorem AlgebraicGeometry.Scheme.Hom.functionFieldMap_algebraMap_stalk {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (f : X ⟶ Y) [IsDominant f] (x : ↥X) (a : ↑(Y.presheaf.stalk (f x))) : (CommRingCat.Hom.hom (functionFieldMap f)) ((algebraMap ↑(Y.presheaf.stalk (f x)) ↑Y.functionField) a) = (algebraMap ↑(X.presheaf.stalk x) ↑X.functionField) ((CategoryTheory.ConcreteCategory.hom (stalkMap f x)) a)

The pullback of rational functions f^* along a dominant morphism f : X ⟶ Y of irreducible schemes is compatible with the maps of stalks: at a point x of X, it sends the image in K(Y) of an element a of 𝒪_{Y,f x} to the image in K(X) of its pullback f^* a ∈ 𝒪_{X,x}.

theorem AlgebraicGeometry.Scheme.Hom.appLE_injective_of_isDominant {X Y : Scheme} [IrreducibleSpace ↥X] [IsIntegral Y] (f : X ⟶ Y) [IsDominant f] (U : Y.Opens) (V : X.Opens) [Nonempty ↥↑V] (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (appLE f U V e))

For a dominant morphism f : X ⟶ Y from an irreducible scheme to an integral scheme, the pullback of sections f.appLE U V e : Γ(Y, U) ⟶ Γ(X, V) is injective as soon as V is nonempty: Γ(Y, U) embeds into the function field K(Y), and f^* : K(Y) ⟶ K(X) is a homomorphism from a field to a nonzero ring.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.functionFieldMap_id {X : Scheme} [IrreducibleSpace ↥X] : functionFieldMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id X.functionField

The pullback of rational functions along the identity is the identity.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.functionFieldMap_comp {X Y Z : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] [IrreducibleSpace ↥Z] (f : X ⟶ Y) (g : Y ⟶ Z) [IsDominant f] [IsDominant g] : functionFieldMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (functionFieldMap g) (functionFieldMap f)

The pullback of rational functions along a composite of dominant morphisms of irreducible schemes is the composite of the pullbacks, in the opposite order.

theorem AlgebraicGeometry.Scheme.Hom.ext_of_functionFieldMap_eq {X Y : Scheme} [IrreducibleSpace ↥X] [IrreducibleSpace ↥Y] (S : Scheme) [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)] {f g : X ⟶ Y} [IsOver f S] [IsOver g S] [IsDominant f] [IsDominant g] (h : functionFieldMap f = functionFieldMap g) : f = g

A dominant morphism into a separated scheme is determined by its pullback of rational functions: two dominant S-morphisms from a reduced irreducible scheme to an irreducible S-scheme separated over S with the same pullback K(Y) ⟶ K(X) are equal.