Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk

{X Y S : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) →
    (sY : Y ⟶ S) →
      [IrreducibleSpace ↥X] →
        [AlgebraicGeometry.LocallyOfFiniteType sY] →
          {x : ↥X} →
            [X.IsGermInjectiveAt x] →
              (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) →
                CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX →
                  X.PartialMap Y

Given S-schemes X and Y such that Y is locally of finite type and X is irreducible germ-injective at x (e.g. when X is integral), any S-morphism Spec 𝒪ₓ ⟶ Y spreads out to a partial map from X to Y.

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

3 results in Mathlib

Foundations

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

Assumes

IrreducibleSpaceAlgebraicGeometry.LocallyOfFiniteTypeAlgebraicGeometry.Scheme.IsGermInjectiveAt