Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.RationalMap.equivFunctionField

{X Y S : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) →
    (sY : Y ⟶ S) →
      [inst : AlgebraicGeometry.IsIntegral X] →
        [AlgebraicGeometry.LocallyOfFiniteType sY] →
          { f //
              CategoryTheory.CategoryStruct.comp f sY =
                CategoryTheory.CategoryStruct.comp (X.fromSpecStalk (genericPoint ↥X)) sX } ≃
            { f // f.compHom sY = AlgebraicGeometry.Scheme.Hom.toRationalMap sX }

Given S-schemes X and Y such that Y is locally of finite type and X is integral, S-morphisms Spec K(X) ⟶ Y correspond bijectively to S-rational maps from X to Y.

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsIntegralAlgebraicGeometry.LocallyOfFiniteType