Theorems · Theorem · algebraic geometry

AlgebraicGeometry.spread_out_of_isGermInjective

∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X}
  [X.IsGermInjectiveAt x] {y : ↥Y} (e : sX x = sY y) (φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap sY y) φ =
      CategoryTheory.CategoryStruct.comp (S.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap sX x) →
    ∃ U,
      ∃ (hxU : x ∈ U),
        ∃ f,
          CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) (Y.fromSpecStalk y) =
              CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧
            CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ι sX

Given S-schemes X Y and points x : X y : Y over s : S. Suppose we have the following diagram of S-schemes `` Spec 𝒪_{X, x} ⟶ X | Spec(φ) ↓ Spec 𝒪_{Y, y} ⟶ Y ` Then the map Spec(φ) spreads out to an S-morphism on an open subscheme U ⊆ X, ` Spec 𝒪_{X, x} ⟶ U ⊆ X | | Spec(φ) | ↓ ↓ Spec 𝒪_{Y, y} ⟶ Y ` provided that Y is locally of finite type over S and X is "germ-injective" at x (e.g. when it's integral or locally Noetherian). TODO: The condition on X is unnecessary when Y` is locally of finite presentation.

Defined in

Mathlib.AlgebraicGeometry.SpreadingOut

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.LocallyOfFiniteTypeAlgebraicGeometry.Scheme.IsGermInjectiveAt