Documentation

Mathlib.AlgebraicGeometry.SpreadingOut

Spreading out morphisms #

Under certain conditions, a morphism on stalks Spec π’ͺ_{X, x} ⟢ Spec π’ͺ_{Y, y} can be spread out into a neighborhood of x.

Main result #

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

We would like to spread Spec(Ο†) out to an S-morphism on an open subscheme U βŠ† X

Spec π’ͺ_{X, x} ⟢ U βŠ† X
    |             |
  Spec(Ο†)         |
    ↓             ↓
Spec π’ͺ_{Y, y} ⟢ Y

TODO #

Show that certain morphism properties can also be spread out.

source
class AlgebraicGeometry.Scheme.IsGermInjectiveAt (X : Scheme) (x : ↑↑X.toPresheafedSpace) :
Prop

The germ map at x is injective if there exists some affine U βˆ‹ x such that the map Ξ“(X, U) ⟢ X_x is injective

Instances
    source
    theorem AlgebraicGeometry.injective_germ_basicOpen {X : Scheme} (U : X.Opens) (hU : IsAffineOpen U) (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U) (f : ↑(X.presheaf.obj (Opposite.op U))) (hf : x ∈ X.basicOpen f) (H : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))) :
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (X.basicOpen f) x hf))
    source
    theorem AlgebraicGeometry.Scheme.exists_germ_injective (X : Scheme) (x : ↑↑X.toPresheafedSpace) [X.IsGermInjectiveAt x] :
    βˆƒ (U : X.Opens) (hx : x ∈ U), IsAffineOpen U ∧ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))
    source
    theorem AlgebraicGeometry.Scheme.exists_le_and_germ_injective (X : Scheme) (x : ↑↑X.toPresheafedSpace) [X.IsGermInjectiveAt x] (V : X.Opens) (hxV : x ∈ V) :
    βˆƒ (U : X.Opens) (hx : x ∈ U), IsAffineOpen U ∧ U ≀ V ∧ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))
    source
    instance AlgebraicGeometry.instIsGermInjectiveAtCoeContinuousMapCarrierCarrierCommRingCatHomTopCatBaseOfIsOpenImmersion {X Y : Scheme} (f : X ⟢ Y) (x : ↑↑X.toPresheafedSpace) [X.IsGermInjectiveAt x] [IsOpenImmersion f] :
    Y.IsGermInjectiveAt ((CategoryTheory.ConcreteCategory.hom f.base) x)
    source
    theorem AlgebraicGeometry.isGermInjectiveAt_iff_of_isOpenImmersion {X Y : Scheme} {f : X ⟢ Y} {x : ↑↑X.toPresheafedSpace} [IsOpenImmersion f] :
    Y.IsGermInjectiveAt ((CategoryTheory.ConcreteCategory.hom f.base) x) ↔ X.IsGermInjectiveAt x
    source
    @[reducible, inline]
    abbrev AlgebraicGeometry.Scheme.IsGermInjective (X : Scheme) :
    Prop

    The class of schemes such that for each x : X, Ξ“(X, U) ⟢ X_x is injective for some affine U containing x.

    This is typically satisfied when X is integral or locally noetherian.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.Scheme.IsGermInjective.of_openCover {X : Scheme} (𝒰 : X.OpenCover) [βˆ€ (i : 𝒰.J), (𝒰.obj i).IsGermInjective] :
      X.IsGermInjective
      source
      theorem AlgebraicGeometry.Scheme.IsGermInjective.Spec {R : CommRingCat} (H : βˆ€ (I : Ideal ↑R), I.IsPrime β†’ βˆƒ f βˆ‰ I, βˆ€ (x y : ↑R), y * x = 0 β†’ y βˆ‰ I β†’ βˆƒ (n : β„•), f ^ n * x = 0) :
      (Spec R).IsGermInjective
      source
      @[instance 100]
      instance AlgebraicGeometry.instIsGermInjectiveOfIsIntegral {X : Scheme} [IsIntegral X] :
      X.IsGermInjective
      source
      @[instance 100]
      instance AlgebraicGeometry.instIsGermInjectiveOfIsLocallyNoetherian {X : Scheme} [IsLocallyNoetherian X] :
      X.IsGermInjective
      source
      theorem AlgebraicGeometry.spread_out_unique_of_isGermInjective {X Y : Scheme} {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (f g : X ⟢ Y) (e : (CategoryTheory.ConcreteCategory.hom f.base) x = (CategoryTheory.ConcreteCategory.hom g.base) x) (H : Scheme.Hom.stalkMap f x = CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes β‹―) (Scheme.Hom.stalkMap g x)) :
      βˆƒ (U : X.Opens), x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ΞΉ f = CategoryTheory.CategoryStruct.comp U.ΞΉ g

      Let x : X and f g : X ⟢ Y be two morphisms such that f x = g x. If f and g agree on the stalk of x, then they agree on an open neighborhood of x, provided 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 type.

      Stacks Tag 0BX6

      source
      theorem AlgebraicGeometry.spread_out_unique_of_isGermInjective' {X Y : Scheme} {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (f g : X ⟢ Y) (e : CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) f = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) g) :
      βˆƒ (U : X.Opens), x ∈ U ∧ CategoryTheory.CategoryStruct.comp U.ΞΉ f = CategoryTheory.CategoryStruct.comp U.ΞΉ g

      A variant of spread_out_unique_of_isGermInjective whose condition is an equality of scheme morphisms instead of ring homomorphisms.

      source
      theorem AlgebraicGeometry.exists_lift_of_germInjective_aux {X : Scheme} {R A : CommRingCat} {U : X.Opens} {x : ↑↑X.toPresheafedSpace} (hxU : x ∈ U) (Ο† : A ⟢ X.presheaf.stalk x) (Ο†RA : R ⟢ A) (Ο†RX : R ⟢ X.presheaf.obj (Opposite.op U)) (hΟ†RA : (CommRingCat.Hom.hom Ο†RA).FiniteType) (e : CategoryTheory.CategoryStruct.comp Ο†RA Ο† = CategoryTheory.CategoryStruct.comp Ο†RX (X.presheaf.germ U x hxU)) :
      βˆƒ (V : X.Opens) (hxV : x ∈ V), V ≀ U ∧ (CommRingCat.Hom.hom Ο†).range ≀ (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)).range
      source
      theorem AlgebraicGeometry.exists_lift_of_germInjective {X : Scheme} {R A : CommRingCat} {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] {U : X.Opens} (hxU : x ∈ U) (Ο† : A ⟢ X.presheaf.stalk x) (Ο†RA : R ⟢ A) (Ο†RX : R ⟢ X.presheaf.obj (Opposite.op U)) (hΟ†RA : (CommRingCat.Hom.hom Ο†RA).FiniteType) (e : CategoryTheory.CategoryStruct.comp Ο†RA Ο† = CategoryTheory.CategoryStruct.comp Ο†RX (X.presheaf.germ U x hxU)) :
      βˆƒ (V : X.Opens) (hxV : x ∈ V) (Ο†' : A ⟢ X.presheaf.obj (Opposite.op V)) (i : V ≀ U), IsAffineOpen V ∧ Ο† = CategoryTheory.CategoryStruct.comp Ο†' (X.presheaf.germ V x hxV) ∧ CategoryTheory.CategoryStruct.comp Ο†RX (X.presheaf.map i.hom.op) = CategoryTheory.CategoryStruct.comp Ο†RA Ο†'

      Suppose X is a scheme, x : X such that the germ map at x is (locally) injective, and U is a neighborhood of x. Given a commutative diagram of CommRingCat

      R ⟢ Ξ“(X, U)
↓    ↓
A ⟢ π’ͺ_{X, x}

      such that R is of finite type over A, we may lift A ⟢ π’ͺ_{X, x} to some A ⟢ Ξ“(X, V).

      source
      theorem AlgebraicGeometry.spread_out_of_isGermInjective {X Y S : Scheme} (sX : X ⟢ S) (sY : Y ⟢ S) [LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] {y : ↑↑Y.toPresheafedSpace} (e : (CategoryTheory.ConcreteCategory.hom sX.base) x = (CategoryTheory.ConcreteCategory.hom sY.base) y) (Ο† : Y.presheaf.stalk y ⟢ X.presheaf.stalk x) (h : CategoryTheory.CategoryStruct.comp (Scheme.Hom.stalkMap sY y) Ο† = CategoryTheory.CategoryStruct.comp (S.presheaf.stalkSpecializes β‹―) (Scheme.Hom.stalkMap sX x)) :
      βˆƒ (U : X.Opens) (hxU : x ∈ U) (f : ↑U ⟢ Y), CategoryTheory.CategoryStruct.comp (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.

      Stacks Tag 0BX6

      source
      theorem AlgebraicGeometry.spread_out_of_isGermInjective' {X Y S : Scheme} (sX : X ⟢ S) (sY : Y ⟢ S) [LocallyOfFiniteType sY] {x : ↑↑X.toPresheafedSpace} [X.IsGermInjectiveAt x] (Ο† : Spec (X.presheaf.stalk x) ⟢ Y) (h : CategoryTheory.CategoryStruct.comp Ο† sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX) :
      βˆƒ (U : X.Opens) (hxU : x ∈ U) (f : ↑U ⟢ Y), Ο† = CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧ CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ΞΉ sX

      Given S-schemes X Y, a point x : X, and a S-morphism Ο† : Spec π’ͺ_{X, x} ⟢ Y, we may spread it out to an S-morphism f : U ⟢ 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.