Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.RationalMap.equivFunctionFieldOver

{X Y S : AlgebraicGeometry.Scheme} →
  [inst : X.Over S] →
    [inst_1 : Y.Over S] →
      [inst_2 : AlgebraicGeometry.IsIntegral X] →
        [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ S)] →
          { f // AlgebraicGeometry.Scheme.Hom.IsOver f S } ≃ { f // AlgebraicGeometry.Scheme.RationalMap.IsOver S f }

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 196 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.OverAlgebraicGeometry.IsIntegralAlgebraicGeometry.LocallyOfFiniteType