Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.RationalMap.ofFunctionField

{X Y S : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) →
    (sY : Y ⟶ S) →
      [inst : AlgebraicGeometry.IsIntegral X] →
        [AlgebraicGeometry.LocallyOfFiniteType sY] →
          (f : AlgebraicGeometry.Spec X.functionField ⟶ Y) →
            CategoryTheory.CategoryStruct.comp f sY =
                CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) sX →
              X.RationalMap Y

Given S-schemes X and Y such that Y is locally of finite type and X is integral, any S-morphism Spec K(X) ⟶ Y spreads out to a rational map from X to Y.

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

1 results in Mathlib

Foundations

Depth 190 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsIntegralAlgebraicGeometry.LocallyOfFiniteType